067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder cd ${1%/*} &> /dev/null && echo $(pwd -P)/${1##*/};
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif [ ! -z $3 ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ -z $1 ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Nothing to translate!" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Cannot find $1" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Cannot read file $TRANS.thy" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederif [ ! -z $2 ]; then
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder ISABELLE="$ISABELLE_BIN_PATH/isabelle"
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroeder if [ ! -e $ISABELLE ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?" > $COMM_FILE
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederif [ ! -x $ISABELLE ]; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:$ISABELLE is not executable" > $COMM_FILE
0d295ebecb355c0f98d3f511619b14156d95e3d4Jonathan von Schroeder if uname | grep Darwin &> /dev/null ; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederecho "v1:Starting Isabelle" > $COMM_FILE
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederimports Datatype FunDef Fixrec Domain
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval out' = fn (f,i,s') =>
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder let val s = \"v\"^(Int.toString i)^\":\"^s'
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder \"/dev/stdin\" => TextIO.output (TextIO.stdOut,s)
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval out = fn (i,s) => out' (\"$COMM_FILE\",i,s);
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederval v = fn s => out (1,\"Isabelle: \"^s);
baacb07fca6a4140974ce2a544edb755ede5a3c2Jonathan von Schroederval e = fn s => (out (0,s); OS.Process.exit OS.Process.failure)
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederv \"Loading helper library\n\";
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederv \"Analyzing theory $TRANS_T\n\";
90bbe729e1e28157a23bd04116e3856cba0b21b3Jonathan von Schroederval thys = Export.xml_of_theory v \"$TRANS.thy\"
90bbe729e1e28157a23bd04116e3856cba0b21b3Jonathan von Schroederhandle ex => e ((General.exnMessage ex)^\"\n\");
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederval xml = XML.Elem ((\"Export\",[]),thys);
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroederv \"Writing theory information\n\";
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder(File.write (Path.explode \"$OUT_FILE\") (XML.string_of xml))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederhandle ex => e ((General.exnMessage ex)^\"\n\");
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder) | ($ISABELLE tty -l HOLCF) | tee $TEMP_FILE
0d295ebecb355c0f98d3f511619b14156d95e3d4Jonathan von Schroederif grep "*** Error" $TEMP_FILE &> /dev/null ; then
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder echo "v0:Loading Theory failed" > $COMM_FILE
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder grep "\*\*\* " $TEMP_FILE | head -n-3 > $COMM_FILE