equal
deleted
inserted
replaced
66 else |
66 else |
67 rm -f "$OUTPUT" |
67 rm -f "$OUTPUT" |
68 "$ISABELLE_PROCESS" \ |
68 "$ISABELLE_PROCESS" \ |
69 -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
69 -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
70 -e "structure Isar = struct fun main () = () end;" \ |
70 -e "structure Isar = struct fun main () = () end;" \ |
71 -e "ml_prompts \"ML> \" \"ML# \";" \ |
|
72 -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ |
71 -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ |
73 -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
72 -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
74 fi |
73 fi |
75 else |
74 else |
76 if [ -z "$OUTPUT" ]; then |
75 if [ -z "$OUTPUT" ]; then |
79 -q RAW_ML_SYSTEM |
78 -q RAW_ML_SYSTEM |
80 else |
79 else |
81 rm -f "$OUTPUT" |
80 rm -f "$OUTPUT" |
82 "$ISABELLE_PROCESS" \ |
81 "$ISABELLE_PROCESS" \ |
83 -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
82 -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
84 -e "ml_prompts \"ML> \" \"ML# \";" \ |
|
85 -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \ |
83 -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \ |
86 -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
84 -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" |
87 fi |
85 fi |
88 fi |
86 fi |
89 |
87 |