protocol support for thread debugger state;

--- a/src/Pure/PIDE/markup.ML	Tue Aug 04 23:11:16 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Aug 05 14:18:07 2015 +0200
@@ -191,6 +191,7 @@
   val build_theories_result: string -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
+  val debugger_state: string -> Properties.T
   val debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
@@ -614,6 +615,7 @@
 
 (* debugger *)
 
+fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
 fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
 
 

--- a/src/Pure/PIDE/markup.scala	Tue Aug 04 23:11:16 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Aug 05 14:18:07 2015 +0200
@@ -495,6 +495,16 @@
 
   /* debugger output */
 
+  val DEBUGGER_STATE = "debugger_state"
+  object Debugger_State
+  {
+    def unapply(props: Properties.T): Option[String] =
+      props match {
+        case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
+        case _ => None
+      }
+  }
+
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {

--- a/src/Pure/Tools/debugger.ML	Tue Aug 04 23:11:16 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Aug 05 14:18:07 2015 +0200
@@ -40,27 +40,27 @@
 
 val global_state = Synchronized.var "Debugger.state" init_state;
 
-fun cancel name =
+fun cancel thread_name =
   Synchronized.change global_state (tap (fn State {threads, ...} =>
-    (case Symtab.lookup threads name of
+    (case Symtab.lookup threads thread_name of
       NONE => ()
     | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
 
-fun input name msg =
+fun input thread_name msg =
   Synchronized.change global_state (map_state (fn (threads, input) =>
-    let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input;
+    let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input;
     in (threads, input') end));
 
-fun get_input name =
+fun get_input thread_name =
   Synchronized.guarded_access global_state (fn State {threads, input} =>
-    (case Symtab.lookup input name of
+    (case Symtab.lookup input thread_name of
       NONE => NONE
     | SOME queue =>
         let
           val (msg, queue') = Queue.dequeue queue;
           val input' =
-            if Queue.is_empty queue' then Symtab.delete_safe name input
-            else Symtab.update (name, queue') input;
+            if Queue.is_empty queue' then Symtab.delete_safe thread_name input
+            else Symtab.update (thread_name, queue') input;
         in SOME (msg, make_state (threads, input')) end));
 
 
@@ -84,13 +84,23 @@
 
 (* main entry point *)
 
-fun debug_loop name =
-  (case get_input name of
+fun debugger_state thread_name =
+  Output.protocol_message (Markup.debugger_state thread_name)
+   [get_data ()
+    |> map (fn st =>
+      (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
+       ML_Debugger.debug_function st))
+    |> let open XML.Encode in list (pair properties string) end
+    |> YXML.string_of_body];
+
+fun debugger_loop thread_name =
+  (debugger_state thread_name;
+   case get_input thread_name of
     ["continue"] => ()
   | bad =>
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad);
-      debug_loop name));
+      debugger_loop thread_name));
 
 fun debugger cond =
   if debugging () orelse not (cond ()) orelse
@@ -100,7 +110,7 @@
     with_debugging (fn () =>
       (case Simple_Thread.get_name () of
         NONE => ()
-      | SOME name => debug_loop name));
+      | SOME thread_name => debugger_loop thread_name));
 
 fun init () =
   ML_Debugger.on_breakpoint
@@ -116,10 +126,10 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.cancel"
-    (fn [name] => cancel name);
+    (fn [thread_name] => cancel thread_name);
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.input"
-    (fn name :: msg => input name msg);
+    (fn thread_name :: msg => input thread_name msg);
 
 end;

--- a/src/Pure/Tools/debugger.scala	Tue Aug 04 23:11:16 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Wed Aug 05 14:18:07 2015 +0200
@@ -11,12 +11,37 @@
 {
   /* global state */
 
+  sealed case class Debug_State(
+    pos: Position.T,
+    function: String)
+
   sealed case class State(
     session: Session = new Session(Resources.empty),
+    threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
-    def add_output(name: String, entry: Command.Results.Entry): State =
-      copy(output = output + (name -> (output.getOrElse(name, Command.Results.empty) + entry)))
+    def set_session(new_session: Session): State =
+      copy(session = new_session)
+
+    def get_thread(thread_name: String): List[Debug_State] =
+      threads.getOrElse(thread_name, Nil)
+
+    def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
+      copy(threads = threads + (thread_name -> debug_states))
+
+    def get_output(thread_name: String): Command.Results =
+      output.getOrElse(thread_name, Command.Results.empty)
+
+    def add_output(thread_name: String, entry: Command.Results.Entry): State =
+      copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
+
+    def clear_output(thread_name: String): State =
+      copy(output = output - thread_name)
+
+    def purge(thread_name: String): State =
+      if (get_thread(thread_name).isEmpty)
+        copy(threads = threads - thread_name, output = output - thread_name)
+      else this
   }
 
   private val global_state = Synchronized(State())
@@ -41,6 +66,25 @@
       delay_update.invoke()
     }
 
+    private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    {
+      msg.properties match {
+        case Markup.Debugger_State(thread_name) =>
+          val msg_body = YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes))
+          val debug_states =
+          {
+            import XML.Decode._
+            list(pair(properties, Symbol.decode_string))(msg_body).map({
+              case (pos, function) => Debug_State(pos, function)
+            })
+          }
+          global_state.change(_.update_thread(thread_name, debug_states))
+          update(thread_name)
+          true
+        case _ => false
+      }
+    }
+
     private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
@@ -61,15 +105,17 @@
     }
 
     val functions =
-      Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
+      Map(
+        Markup.DEBUGGER_STATE -> debugger_state _,
+        Markup.DEBUGGER_OUTPUT -> debugger_output _)
   }
 
 
   /* protocol commands */
 
-  def init(new_session: Session)
+  def init(session: Session)
   {
-    global_state.change(_.copy(session = new_session))
+    global_state.change(_.set_session(session))
     current_state().session.protocol_command("Debugger.init")
   }
 

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 04 23:11:16 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 14:18:07 2015 +0200
@@ -94,7 +94,7 @@
     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
     val new_output =  // FIXME select by thread name
       (for ((_, results) <- Debugger.current_state.output; (_, tree) <- results.iterator)
-        yield tree).toList
+        yield tree).toList ::: List(XML.Text(Debugger.current_state.threads.toString))
 
     if (new_output != current_output)
       pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))