src/Pure/System/isabelle_process.ML
changeset 52655 3b2b1ef13979
parent 52584 5cad4a5f5615
child 52710 52790e3961fe
     1.1 --- a/src/Pure/System/isabelle_process.ML	Sun Jul 14 00:08:15 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Jul 15 10:25:35 2013 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  sig
     1.5    val is_active: unit -> bool
     1.6    val protocol_command: string -> (string list -> unit) -> unit
     1.7 -  val reset_tracing: unit -> unit
     1.8 +  val reset_tracing: Document_ID.exec -> unit
     1.9    val crashes: exn list Synchronized.var
    1.10    val init_fifos: string -> string -> unit
    1.11    val init_socket: string -> unit
    1.12 @@ -67,20 +67,20 @@
    1.13  val tracing_messages =
    1.14    Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
    1.15  
    1.16 -fun reset_tracing () =
    1.17 -  Synchronized.change tracing_messages (K Inttab.empty);
    1.18 +fun reset_tracing exec_id =
    1.19 +  Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
    1.20  
    1.21  fun update_tracing () =
    1.22    (case Position.parse_id (Position.thread_data ()) of
    1.23      NONE => ()
    1.24 -  | SOME id =>
    1.25 +  | SOME exec_id =>
    1.26        let
    1.27          val ok =
    1.28            Synchronized.change_result tracing_messages (fn tab =>
    1.29              let
    1.30 -              val n = the_default 0 (Inttab.lookup tab id) + 1;
    1.31 +              val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
    1.32                val ok = n <= Options.default_int "editor_tracing_messages";
    1.33 -            in (ok, Inttab.update (id, n) tab) end);
    1.34 +            in (ok, Inttab.update (exec_id, n) tab) end);
    1.35        in
    1.36          if ok then ()
    1.37          else
    1.38 @@ -93,7 +93,7 @@
    1.39                handle Fail _ => error "Stopped";
    1.40            in
    1.41              Synchronized.change tracing_messages
    1.42 -              (Inttab.map_default (id, 0) (fn k => k - m))
    1.43 +              (Inttab.map_default (exec_id, 0) (fn k => k - m))
    1.44            end
    1.45        end);
    1.46