# HG changeset patch
# User wenzelm
# Date 1369152216 -7200
# Node ID 88b423034d4f144b07a91abb575b556dc16af9fd
# Parent  250cd2a9308dbeee8c4ba71f36ae2c5386423694
proper options;
tuned;

diff -r 250cd2a9308d -r 88b423034d4f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue May 21 17:55:28 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue May 21 18:03:36 2013 +0200
@@ -17,7 +17,6 @@
 sig
   val is_active: unit -> bool
   val protocol_command: string -> (string list -> unit) -> unit
-  val tracing_messages: int Unsynchronized.ref;
   val reset_tracing: unit -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
@@ -65,13 +64,11 @@
 
 (* restricted tracing messages *)
 
-val tracing_messages = Unsynchronized.ref 100;
-
-val command_tracing_messages =
-  Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table);
+val tracing_messages =
+  Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
 
 fun reset_tracing () =
-  Synchronized.change command_tracing_messages (K Inttab.empty);
+  Synchronized.change tracing_messages (K Inttab.empty);
 
 fun update_tracing () =
   (case Position.parse_id (Position.thread_data ()) of
@@ -79,10 +76,10 @@
   | SOME id =>
       let
         val (n, ok) =
-          Synchronized.change_result command_tracing_messages (fn tab =>
+          Synchronized.change_result tracing_messages (fn tab =>
             let
               val n = the_default 0 (Inttab.lookup tab id) + 1;
-              val ok = n <= ! tracing_messages;
+              val ok = n <= Options.default_int "editor_tracing_messages";
             in ((n, ok), Inttab.update (id, n) tab) end);
       in
         if ok then ()
@@ -95,7 +92,7 @@
             val m = Markup.parse_int (Future.join promise)
               handle Fail _ => error "Stopped";
           in
-            Synchronized.change command_tracing_messages
+            Synchronized.change tracing_messages
               (Inttab.map_default (id, 0) (fn k => k - m))
           end
       end);
@@ -243,8 +240,7 @@
         if Multithreading.max_threads_value () < 2
         then Multithreading.max_threads := 2 else ();
         Goal.skip_proofs := Options.bool options "editor_skip_proofs";
-        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
-        tracing_messages := Options.int options "editor_tracing_messages"
+        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
       end);
 
 end;