export.sh revision 6df4343f46cc159371dfa671c5943354480f4e1c
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
eca83bf7d98670ee4fa52661d2f8222429a4f91aJonathan von Schroederimports Datatype FunDef
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);
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederval v = fn s => out (1,s);
705d8c3d5549a00d4b00e0cb80e3a77441f85267Jonathan von Schroederval e = fn s => out (0,s);
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederv \"Isabelle: Loading helper library\n\";
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederv \"Isabelle: Analyzing theory\n\";
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederval thy = Parser.scan \"$TRANS.thy\" |> Parser.thy;
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroederv \"Isabelle: Exporting theory information\n\";
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder(File.write (Path.explode \"$OUT_FILE\")
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (XML.string_of (Export.xml_of_theory thy)))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederhandle ex => e ((General.exnMessage ex)^\"\n\");
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