src/Pure/System/isabelle_process.ML

--- a/src/Pure/System/isabelle_process.ML	Sun Jul 14 00:08:15 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Jul 15 10:25:35 2013 +0200
@@ -17,7 +17,7 @@
 sig
   val is_active: unit -> bool
   val protocol_command: string -> (string list -> unit) -> unit
-  val reset_tracing: unit -> unit
+  val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
   val init_socket: string -> unit
@@ -67,20 +67,20 @@
 val tracing_messages =
   Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
 
-fun reset_tracing () =
-  Synchronized.change tracing_messages (K Inttab.empty);
+fun reset_tracing exec_id =
+  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
 
 fun update_tracing () =
   (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
-  | SOME id =>
+  | SOME exec_id =>
       let
         val ok =
           Synchronized.change_result tracing_messages (fn tab =>
             let
-              val n = the_default 0 (Inttab.lookup tab id) + 1;
+              val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
               val ok = n <= Options.default_int "editor_tracing_messages";
-            in (ok, Inttab.update (id, n) tab) end);
+            in (ok, Inttab.update (exec_id, n) tab) end);
       in
         if ok then ()
         else
@@ -93,7 +93,7 @@
               handle Fail _ => error "Stopped";
           in
             Synchronized.change tracing_messages
-              (Inttab.map_default (id, 0) (fn k => k - m))
+              (Inttab.map_default (exec_id, 0) (fn k => k - m))
           end
       end);