src/Pure/Tools/debugger.scala

--- a/src/Pure/Tools/debugger.scala	Thu Jul 30 11:39:30 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Thu Jul 30 14:02:19 2015 +0200
@@ -11,7 +11,8 @@
 {
   /* global state */
 
-  case class State(
+  sealed case class State(
+    session: Session = new Session(Resources.empty),
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
     def add_output(name: String, entry: Command.Results.Entry): State =
@@ -22,42 +23,36 @@
   def current_state(): State = global_state.value
 
 
-  /* GUI interaction */
-
-  case object Event
-
-
-  /* manager thread */
+  /* protocol handler */
 
-  private lazy val manager: Consumer_Thread[Any] =
-    Consumer_Thread.fork[Any]("Debugger.manager", daemon = true)(
-      consume = (arg: Any) =>
-      {
-        // FIXME
-        true
-      },
-      finish = () =>
-      {
-        // FIXME
-      }
-    )
-
-
-  /* protocol handler */
+  sealed case class Update(thread_names: Set[String])
 
   class Handler extends Session.Protocol_Handler
   {
+    private var updated = Set.empty[String]
+    private val delay_update =
+      Simple_Thread.delay_first(current_state().session.output_delay) {
+        current_state().session.debugger_updates.post(Update(updated))
+        updated = Set.empty
+      }
+    private def update(name: String)
+    {
+      updated += name
+      delay_update.invoke()
+    }
+
     private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
-        case Markup.Debugger_Output(name) =>
+        case Markup.Debugger_Output(thread_name) =>
           val msg_body =
             prover.xml_cache.body(
               YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
           msg_body match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
-              global_state.change(_.add_output(name, i -> message))
+              global_state.change(_.add_output(thread_name, i -> message))
+              update(thread_name)
               true
             case _ => false
           }
@@ -65,11 +60,6 @@
       }
     }
 
-    override def stop(prover: Prover)
-    {
-      manager.shutdown()
-    }
-
     val functions =
       Map(Markup.DEBUGGER_OUTPUT -> debugger_output _)
   }
@@ -77,12 +67,15 @@
 
   /* protocol commands */
 
-  def init(session: Session): Unit =
-    session.protocol_command("Debugger.init")
+  def init(new_session: Session)
+  {
+    global_state.change(_.copy(session = new_session))
+    current_state().session.protocol_command("Debugger.init")
+  }
 
-  def cancel(session: Session, name: String): Unit =
-    session.protocol_command("Debugger.cancel", name)
+  def cancel(name: String): Unit =
+    current_state().session.protocol_command("Debugger.cancel", name)
 
-  def input(session: Session, name: String, msg: String*): Unit =
-    session.protocol_command("Debugger.input", (name :: msg.toList):_*)
+  def input(name: String, msg: String*): Unit =
+    current_state().session.protocol_command("Debugger.input", (name :: msg.toList):_*)
 }