equal
deleted
inserted
replaced
59 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
59 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
60 |
60 |
61 if [ "$TARGET" = RAW ]; then |
61 if [ "$TARGET" = RAW ]; then |
62 if [ -z "$OUTPUT" ]; then |
62 if [ -z "$OUTPUT" ]; then |
63 "$ISABELLE_PROCESS" \ |
63 "$ISABELLE_PROCESS" \ |
64 -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
64 -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \ |
65 -q RAW_ML_SYSTEM |
65 -q RAW_ML_SYSTEM |
66 else |
66 else |
67 "$ISABELLE_PROCESS" \ |
67 "$ISABELLE_PROCESS" \ |
68 -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ |
68 -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \ |
69 -e "structure Isar = struct fun main () = () end;" \ |
69 -e "structure Isar = struct fun main () = () end;" \ |
70 -e "ml_prompts \"ML> \" \"ML# \";" \ |
70 -e "ml_prompts \"ML> \" \"ML# \";" \ |
71 -q -w RAW_ML_SYSTEM "$OUTPUT" |
71 -q -w RAW_ML_SYSTEM "$OUTPUT" |
72 fi |
72 fi |
73 else |
73 else |
74 if [ -z "$OUTPUT" ]; then |
74 if [ -z "$OUTPUT" ]; then |
75 "$ISABELLE_PROCESS" \ |
75 "$ISABELLE_PROCESS" \ |
76 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
76 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ |
77 -q RAW_ML_SYSTEM |
77 -q RAW_ML_SYSTEM |
78 else |
78 else |
79 "$ISABELLE_PROCESS" \ |
79 "$ISABELLE_PROCESS" \ |
80 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ |
80 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ |
81 -e "ml_prompts \"ML> \" \"ML# \";" \ |
81 -e "ml_prompts \"ML> \" \"ML# \";" \ |
82 -f -q -w RAW_ML_SYSTEM "$OUTPUT" |
82 -f -q -w RAW_ML_SYSTEM "$OUTPUT" |
83 fi |
83 fi |
84 fi |
84 fi |
85 |
85 |