diff -r f37b02353519 -r 1b56b5471c7d src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Tue Feb 28 17:12:39 2023 +0100 +++ b/src/Pure/ML/ml_process.scala Tue Feb 28 17:16:50 2023 +0100 @@ -58,10 +58,11 @@ "PolyML.Compiler.prompt1 := \"Poly/ML> \"", "PolyML.Compiler.prompt2 := \"Poly/ML# \"") } - else + else { List( "(PolyML.SaveState.loadHierarchy " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0)") + } val eval_modes = if (modes.isEmpty) Nil