# HG changeset patch # User wenzelm # Date 1460306509 -7200 # Node ID 5612ec9f0f494637712105ea6962f4fbcbe09888 # Parent a03592aafadf61f6876605ee852508397476fdb6 proper support for recursive ML debugging; diff -r a03592aafadf -r 5612ec9f0f49 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Sun Apr 10 17:52:30 2016 +0200 +++ b/src/Pure/ML/ml_compiler.ML Sun Apr 10 18:41:49 2016 +0200 @@ -48,7 +48,7 @@ |> Position.of_properties) end; -fun report_parse_tree redirect depth space parse_tree = +fun report_parse_tree redirect depth name_space parse_tree = let val is_visible = (case Context.get_generic_context () of @@ -64,7 +64,7 @@ is_reported pos ? let val xml = - PolyML.NameSpace.Values.printType (types, depth, SOME space) + PolyML.NameSpace.Values.printType (types, depth, SOME name_space) |> Pretty.from_polyml |> Pretty.string_of |> Output.output |> YXML.parse_body; in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end @@ -133,23 +133,26 @@ val all_breakpoints = rev (breakpoints_tree parse_tree []); val _ = Position.reports (map #1 all_breakpoints); - val _ = - if is_some (Context.get_generic_context ()) then - Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints) - else (); - in () end; + in map (fn (_, (id, (b, pos))) => (id, (b, Position.dest pos))) all_breakpoints end; (* eval ML source tokens *) fun eval (flags: flags) pos toks = let - val space = - (case (#SML flags orelse #exchange flags, ML_Recursive.get ()) of - (false, SOME space) => space - | _ => ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags}); val opt_context = Context.get_generic_context (); + val env as {debug, name_space, add_breakpoints} = + (case (ML_Recursive.get (), #SML flags orelse #exchange flags) of + (SOME env, false) => env + | _ => + {debug = + (case #debug flags of + SOME debug => debug + | NONE => ML_Options.debugger_enabled opt_context), + name_space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags}, + add_breakpoints = ML_Env.add_breakpoints}); + (* input *) @@ -211,20 +214,23 @@ else (); fun apply_fix (a, b) = - (#enterFix space (a, b); display PolyML.NameSpace.Infixes.print b); + (#enterFix name_space (a, b); + display PolyML.NameSpace.Infixes.print b); fun apply_type (a, b) = - (#enterType space (a, b); - display PolyML.NameSpace.TypeConstrs.print (b, depth, SOME space)); + (#enterType name_space (a, b); + display PolyML.NameSpace.TypeConstrs.print (b, depth, SOME name_space)); fun apply_sig (a, b) = - (#enterSig space (a, b); display PolyML.NameSpace.Signatures.print (b, depth, SOME space)); + (#enterSig name_space (a, b); + display PolyML.NameSpace.Signatures.print (b, depth, SOME name_space)); fun apply_struct (a, b) = - (#enterStruct space (a, b); - display PolyML.NameSpace.Structures.print (b, depth, SOME space)); + (#enterStruct name_space (a, b); + display PolyML.NameSpace.Structures.print (b, depth, SOME name_space)); fun apply_funct (a, b) = - (#enterFunct space (a, b); display PolyML.NameSpace.Functors.print (b, depth, SOME space)); + (#enterFunct name_space (a, b); + display PolyML.NameSpace.Functors.print (b, depth, SOME name_space)); fun apply_val (a, b) = - (#enterVal space (a, b); - display PolyML.NameSpace.Values.printWithType (b, depth, SOME space)); + (#enterVal name_space (a, b); + display PolyML.NameSpace.Values.printWithType (b, depth, SOME name_space)); in List.app apply_fix fixes; List.app apply_type types; @@ -239,7 +245,8 @@ fun result_fun (phase1, phase2) () = ((case phase1 of NONE => () - | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree); + | SOME parse_tree => + add_breakpoints (report_parse_tree (#redirect flags) depth name_space parse_tree)); (case phase2 of NONE => raise STATIC_ERRORS () | SOME code => @@ -251,14 +258,9 @@ (* compiler invocation *) - val debug = - (case #debug flags of - SOME debug => debug - | NONE => ML_Options.debugger_enabled opt_context); - val parameters = [PolyML.Compiler.CPOutStream write, - PolyML.Compiler.CPNameSpace space, + PolyML.Compiler.CPNameSpace name_space, PolyML.Compiler.CPErrorMessageProc message, PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), @@ -270,7 +272,7 @@ val _ = (while not (List.null (! input_buffer)) do - ML_Recursive.recursive space (fn () => PolyML.compiler (get, parameters) ())) + ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ())) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else diff -r a03592aafadf -r 5612ec9f0f49 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Sun Apr 10 17:52:30 2016 +0200 +++ b/src/Pure/ML/ml_env.ML Sun Apr 10 18:41:49 2016 +0200 @@ -9,9 +9,8 @@ sig val inherit: Context.generic -> Context.generic -> Context.generic val forget_structure: string -> Context.generic -> Context.generic - val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) -> - Context.generic -> Context.generic val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option + val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit val init_bootstrap: Context.generic -> Context.generic val SML_environment: bool Config.T val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic @@ -84,12 +83,16 @@ (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables); in make_data (bootstrap, tables', sml_tables, breakpoints) end); -fun add_breakpoint breakpoint = - Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => - let val breakpoints' = Inttab.update_new breakpoint breakpoints; - in make_data (bootstrap, tables, sml_tables, breakpoints') end); +val get_breakpoint = Inttab.lookup o #breakpoints o Env.get; -val get_breakpoint = Inttab.lookup o #breakpoints o Env.get; +fun add_breakpoints more_breakpoints = + if is_some (Context.get_generic_context ()) then + Context.>> + (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + let val breakpoints' = + fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints breakpoints; + in make_data (bootstrap, tables, sml_tables, breakpoints') end)) + else (); (* SML environment for Isabelle/ML *) diff -r a03592aafadf -r 5612ec9f0f49 src/Pure/ML/ml_recursive.ML --- a/src/Pure/ML/ml_recursive.ML Sun Apr 10 17:52:30 2016 +0200 +++ b/src/Pure/ML/ml_recursive.ML Sun Apr 10 18:41:49 2016 +0200 @@ -6,14 +6,23 @@ signature ML_RECURSIVE = sig - val get: unit -> PolyML.NameSpace.nameSpace option - val recursive: PolyML.NameSpace.nameSpace -> (unit -> 'a) -> 'a + type env = + {debug: bool, + name_space: PolyML.NameSpace.nameSpace, + add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit}; + val get: unit -> env option + val recursive: env -> (unit -> 'a) -> 'a end; structure ML_Recursive: ML_RECURSIVE = struct -val var = Thread_Data.var () : PolyML.NameSpace.nameSpace Thread_Data.var; +type env = + {debug: bool, + name_space: PolyML.NameSpace.nameSpace, + add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit}; + +val var = Thread_Data.var () : env Thread_Data.var; fun get () = Thread_Data.get var; fun recursive space e = Thread_Data.setmp var (SOME space) e ();