support for ML debugger;

--- a/etc/options	Tue Jul 21 14:12:45 2015 +0200
+++ b/etc/options	Tue Jul 21 19:04:36 2015 +0200
@@ -104,6 +104,12 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
+public option ML_debugger_active : bool = false
+  -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
+
+public option ML_debugger_stepping : bool = false
+  -- "ML debugger in single-step mode"
+
 public option ML_statistics : bool = true
   -- "ML runtime system statistics"
 

--- a/src/Pure/Tools/debugger.ML	Tue Jul 21 14:12:45 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Jul 21 19:04:36 2015 +0200
@@ -4,13 +4,103 @@
 Interactive debugger for Isabelle/ML.
 *)
 
-signature DEBUGGER =
-sig
+structure Debugger: sig end =
+struct
+
+(* global state *)
+
+datatype state =
+  State of {
+    threads: Thread.thread Symtab.table,  (*thread identification ~> thread*)
+    input: string list Queue.T Symtab.table  (*thread identification ~> input queue*)
+  };
+
+fun make_state (threads, input) = State {threads = threads, input = input};
+val init_state = make_state (Symtab.empty, Symtab.empty);
+fun map_state f (State {threads, input}) = make_state (f (threads, input));
+
+val global_state = Synchronized.var "Debugger.state" init_state;
+
+fun cancel id =
+  Synchronized.change global_state (tap (fn State {threads, ...} =>
+    (case Symtab.lookup threads id of
+      NONE => ()
+    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
+
+fun input id msg =
+  Synchronized.change global_state (map_state (fn (threads, input) =>
+    let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input;
+    in (threads, input') end));
+
+fun get_input id =
+  Synchronized.guarded_access global_state (fn State {threads, input} =>
+    (case Symtab.lookup input id of
+      NONE => NONE
+    | SOME queue =>
+        let
+          val (msg, queue') = Queue.dequeue queue;
+          val input' =
+            if Queue.is_empty queue' then Symtab.delete_safe id input
+            else Symtab.update (id, queue') input;
+        in SOME (msg, make_state (threads, input')) end));
+
+
+(* thread data *)
+
+local val tag = Universal.tag () : ML_Debugger.state list Universal.tag in
+
+fun get_data () = the_default [] (Thread.getLocal tag);
+fun setmp_data data f x = setmp_thread_data tag (get_data ()) data f x;
+
 end;
 
-structure Debugger: DEBUGGER =
-struct
+val debugging = not o null o get_data;
+fun with_debugging e = setmp_data (ML_Debugger.state (Thread.self ())) e ();
+
+
+(* protocol messages *)
 
 val _ = Session.protocol_handler "isabelle.Debugger$Handler";
 
+
+(* main entry point *)
+
+fun debug_loop id =
+  (case get_input id of
+    ["continue"] => ()
+  | bad =>
+     (Output.system_message
+        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
+      debug_loop id));
+
+fun debugger cond =
+  if debugging () orelse not (cond ()) orelse
+    not (Options.default_bool @{system_option ML_debugger_active})
+  then ()
+  else
+    with_debugging (fn () =>
+      (case Simple_Thread.identification () of
+        NONE => ()
+      | SOME id => debug_loop id));
+
+fun init () =
+  ML_Debugger.on_breakpoint
+    (SOME (fn (_, b) =>
+      debugger (fn () => ! b orelse Options.default_bool @{system_option ML_debugger_stepping})));
+
+
+(* protocol commands *)
+
+val _ =
+  Isabelle_Process.protocol_command "Debugger.init"
+    (fn [] => init ());
+
+val _ =
+  Isabelle_Process.protocol_command "Debugger.cancel"
+    (fn [id] => cancel id);
+
+val _ =
+  Isabelle_Process.protocol_command "Debugger.input"
+    (fn id :: msg => input id msg);
+
 end;

--- a/src/Pure/Tools/debugger.scala	Tue Jul 21 14:12:45 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Jul 21 19:04:36 2015 +0200
@@ -41,4 +41,16 @@
 
     val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean]  // FIXME
   }
+
+
+  /* protocol commands */
+
+  def init(session: Session): Unit =
+    session.protocol_command("Debugger.init")
+
+  def cancel(session: Session, id: String): Unit =
+    session.protocol_command("Debugger.cancel", id)
+
+  def input(session: Session, id: String, msg: String*): Unit =
+    session.protocol_command("Debugger.input", (id :: msg.toList):_*)
 }