proper support for recursive ML debugging;

--- 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

--- 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 *)

--- 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 ();