export.sh revision 7bbfb15142ab4286dfc6fcde2fc94a5512297e41
# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
if [ -z $1 ]; then
echo "Nothing to translate!"
exit 1
fi
if [ ! -z $2 ]; then
OUT_FILE="$2"
fi
echo "Cannot read file $TRANS.thy"
exit 1
fi
if [ ! -z $ISABELLE_BIN_PATH ]; then
ISABELLE="$ISABELLE_BIN_PATH/isabelle"
if [ ! -e $ISABELLE ]; then
echo "Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?"
fi
else
else
echo "Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?"
exit 1
fi
fi
if [ ! -x $ISABELLE ]; then
echo "$ISABELLE is not executable"
exit 1
fi
if [ -z $OUT_FILE ]; then
fi
echo $ISABELLE
(
echo "theory IsaExport"
echo "imports \"$TRANS\" Wellfounded"
echo "uses \"$SCRIPTPATH/export_helper.ml\""
echo "begin"
echo "ML {*"
echo "val T = Thy_Info.get_theory \"$TRANS_T\";
val xml = ExportHelper.tinfo2xml T \"$TRANS_T\"
(ExportHelper.theory_info T);
File.write (Path.explode \"$OUT_FILE\") (XML.string_of xml);
"
echo "*}"
echo "end;"