equal
deleted
inserted
replaced
113 |
113 |
114 function generate_dot() |
114 function generate_dot() |
115 { |
115 { |
116 LOADER="tptp_graph_$RANDOM" |
116 LOADER="tptp_graph_$RANDOM" |
117 echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \ |
117 echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \ |
118 uses \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ |
118 begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ |
119 begin ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ |
119 ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ |
120 > $WORKDIR/$LOADER.thy |
120 > $WORKDIR/$LOADER.thy |
121 "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\"; exit 0;" Pure |
121 "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\"; exit 0;" Pure |
122 } |
122 } |
123 |
123 |
124 function cleanup_workdir() |
124 function cleanup_workdir() |