changeset 80809 | 4a64fc4d1cde |
parent 78728 | 72631efa3821 |
--- a/src/Pure/Tools/debugger.ML Wed Sep 04 16:21:52 2024 +0200 +++ b/src/Pure/Tools/debugger.ML Thu Sep 05 17:39:45 2024 +0200 @@ -183,7 +183,7 @@ val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index); fun print x = - Pretty.from_polyml + Pretty.from_ML (PolyML.NameSpace.Values.printWithType (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space)); fun print_all () =