--- a/src/Pure/ML/ml_process.scala Tue Feb 28 16:25:23 2023 +0100
+++ b/src/Pure/ML/ml_process.scala Tue Feb 28 17:12:39 2023 +0100
@@ -61,10 +61,7 @@
else
List(
"(PolyML.SaveState.loadHierarchy " +
- ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
- "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
- ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
- "); OS.Process.exit OS.Process.failure)")
+ ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0)")
val eval_modes =
if (modes.isEmpty) Nil