export.sh revision eca83bf7d98670ee4fa52661d2f8222429a4f91a
# 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
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,s);
val e = fn s => out (0,s);
v \"Isabelle: Loading theory $TRANS\n\";
use_thy \"$TRANS\";
v \"Isabelle: Loading helper library\n\";
use \"$SCRIPTPATH/export_helper.ml\";
val T = Thy_Info.get_theory \"$TRANS_T\";
v \"Isabelle: Exporting theory information\n\";
(File.write (Path.explode \"$OUT_FILE\")
(XML.string_of (ExportHelper.tinfo2xml T \"$TRANS_T\"
(ExportHelper.theory_info T))))
handle ExportHelper.ExportError msg => e (msg^\"\n\");
*}
end"
echo "v0:Loading Theory failed" > $COMM_FILE
exit 1
fi