00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder cd ${1%/*} &> /dev/null && echo $(pwd -P)/${1##*/};
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif [ -z $1 ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Nothing to translate!"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot find $1"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot read file $TRANS.thy"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder ISABELLE="$ISABELLE_BIN_PATH/isabelle"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder if [ ! -e $ISABELLE ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif [ ! -x $ISABELLE ]; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "$ISABELLE is not executable"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder if uname | grep Darwin &> /dev/null ; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederecho "Starting Isabelle"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederimports Datatype FunDef
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederval s = File.read (Path.explode \"$TRANS.thy\");
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederval (th,err) = Parser.scan s |> Parser.test;
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von SchroederFile.write (Path.explode \"./test.out\") (Parser.scan s |> PolyML.makestring);
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederif grep "*** Error" $TEMP_FILE &> /dev/null ; then
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "Loading Theory failed"
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder grep "\*\*\* " $TEMP_FILE | head -n-3