# ISABELLE_BIN_PATH (if isabelle is not located in PATH)
if [ "${1%/*}" = "${1##*/}" ]; then
echo $(pwd -P)/$1
else
local P=`pwd`;
local R=$?;
return $R;
fi
}
if [ ! -z $3 ]; then
COMM_FILE="$3"
else
fi
if [ -z $1 ]; then
echo "v0:Nothing to translate!" > $COMM_FILE
exit 1
fi
echo "v0:Cannot find $1" > $COMM_FILE
exit 1
fi
echo "v0:Cannot read file $TRANS.thy" > $COMM_FILE
exit 1
fi
if [ ! -z $2 ]; then
OUT_FILE="$2"
else
fi
if [ ! -z $ISABELLE_BIN_PATH ]; then
ISABELLE="$ISABELLE_BIN_PATH/isabelle"
if [ ! -e $ISABELLE ]; then
echo "v0:Cannot find isabelle executable. Maybe you didn't specify ISABELLE_BIN_PATH correctly?" > $COMM_FILE
exit 1
fi
else
else
echo "v0:Cannot find isabelle executable. Maybe you need to specify ISABELLE_BIN_PATH?" > $COMM_FILE
exit 1
fi
fi
if [ ! -x $ISABELLE ]; then
echo "v0:$ISABELLE is not executable" > $COMM_FILE
exit 1
fi
else
fi
else
fi
echo "v1:Starting Isabelle" > $COMM_FILE
(
echo "theory IsaExport
imports Datatype FunDef Fixrec Domain
begin
ML {*
val out' = fn (f,i,s') =>
let val s = \"v\"^(Int.toString i)^\":\"^s'
in case f of
\"/dev/stdin\" => TextIO.output (TextIO.stdOut,s)
| _ => File.write (Path.explode f) s
end;
val out = fn (i,s) => out' (\"$COMM_FILE\",i,s);
val v = fn s => out (1,\"Isabelle: \"^s);
val e = fn s => (out (0,s); OS.Process.exit OS.Process.failure)
v \"Loading helper library\n\";
use \"$SCRIPTPATH/parser.ml\";
v \"Analyzing theory $TRANS_T\n\";
val thys = Export.xml_of_theory v \"$TRANS.thy\"
handle ex => e ((General.exnMessage ex)^\"\n\");
val xml = XML.Elem ((\"Export\",[]),thys);
v \"Writing theory information\n\";
(File.write (Path.explode \"$OUT_FILE\") (XML.string_of xml))
handle ex => e ((General.exnMessage ex)^\"\n\");
*}
end"
echo "v0:Loading Theory failed" > $COMM_FILE
exit 1
fi