author | wenzelm |
Tue, 28 Feb 2023 17:16:50 +0100 | |
changeset 77413 | 1b56b5471c7d |
parent 77412 | f37b02353519 |
child 77414 | 0d5994eef9e6 |
--- 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