suppress threads without debug state;
authorwenzelm
Tue, 11 Aug 2015 21:24:11 +0200
changeset 60903 bca464396b80
parent 60902 9f185acfdcb8
child 60904 e0fab97c989f
suppress threads without debug state;
src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 21:15:29 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 21:24:11 2015 +0200
@@ -45,7 +45,8 @@
       threads.getOrElse(thread_name, Nil)
 
     def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
-      copy(threads = threads + (thread_name -> debug_states))
+      if (debug_states.isEmpty) copy(threads = threads - thread_name)
+      else copy(threads = threads + (thread_name -> debug_states))
 
     def get_output(thread_name: String): Command.Results =
       output.getOrElse(thread_name, Command.Results.empty)