# HG changeset patch
# User wenzelm
# Date 1439320529 -7200
# Node ID 9f185acfdcb860149be96e20a8a65b8687f08a3d
# Parent  ce8abd005c5deacae0af92746c06bf7802607f39
clarified events;
tuned signature;

diff -r ce8abd005c5d -r 9f185acfdcb8 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 20:49:22 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 21:15:29 2015 +0200
@@ -55,27 +55,25 @@
 
     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())
 
 
-  /* protocol handler */
+  /* update events */
 
   case object Update
 
+  private val delay_update =
+    Simple_Thread.delay_first(global_state.value.session.output_delay) {
+      global_state.value.session.debugger_updates.post(Update)
+    }
+
+
+  /* protocol handler */
+
   class Handler extends Session.Protocol_Handler
   {
-    private val delay_update =
-      Simple_Thread.delay_first(global_state.value.session.output_delay) {
-        global_state.value.session.debugger_updates.post(Update)
-      }
-
     private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
@@ -189,6 +187,7 @@
   def clear_output(thread_name: String)
   {
     global_state.change(_.clear_output(thread_name))
+    delay_update.invoke()
   }
 
   def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String)
@@ -198,6 +197,7 @@
         index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression))
       state.clear_output(thread_name)
     })
+    delay_update.invoke()
   }
 
   def print_vals(thread_name: String, index: Int, SML: Boolean, context: String)
@@ -206,5 +206,6 @@
       input(thread_name, "print_vals", index.toString, SML.toString, Symbol.encode(context))
       state.clear_output(thread_name)
     })
+    delay_update.invoke()
   }
 }