proper options;
authorwenzelm
Tue May 21 18:03:36 2013 +0200 (2013-05-21 ago)
changeset 5210588b423034d4f
parent 52104 250cd2a9308d
child 52106 090a519982e9
proper options;
tuned;
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/System/isabelle_process.ML	Tue May 21 17:55:28 2013 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue May 21 18:03:36 2013 +0200
     1.3 @@ -17,7 +17,6 @@
     1.4  sig
     1.5    val is_active: unit -> bool
     1.6    val protocol_command: string -> (string list -> unit) -> unit
     1.7 -  val tracing_messages: int Unsynchronized.ref;
     1.8    val reset_tracing: unit -> unit
     1.9    val crashes: exn list Synchronized.var
    1.10    val init_fifos: string -> string -> unit
    1.11 @@ -65,13 +64,11 @@
    1.12  
    1.13  (* restricted tracing messages *)
    1.14  
    1.15 -val tracing_messages = Unsynchronized.ref 100;
    1.16 -
    1.17 -val command_tracing_messages =
    1.18 -  Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table);
    1.19 +val tracing_messages =
    1.20 +  Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
    1.21  
    1.22  fun reset_tracing () =
    1.23 -  Synchronized.change command_tracing_messages (K Inttab.empty);
    1.24 +  Synchronized.change tracing_messages (K Inttab.empty);
    1.25  
    1.26  fun update_tracing () =
    1.27    (case Position.parse_id (Position.thread_data ()) of
    1.28 @@ -79,10 +76,10 @@
    1.29    | SOME id =>
    1.30        let
    1.31          val (n, ok) =
    1.32 -          Synchronized.change_result command_tracing_messages (fn tab =>
    1.33 +          Synchronized.change_result tracing_messages (fn tab =>
    1.34              let
    1.35                val n = the_default 0 (Inttab.lookup tab id) + 1;
    1.36 -              val ok = n <= ! tracing_messages;
    1.37 +              val ok = n <= Options.default_int "editor_tracing_messages";
    1.38              in ((n, ok), Inttab.update (id, n) tab) end);
    1.39        in
    1.40          if ok then ()
    1.41 @@ -95,7 +92,7 @@
    1.42              val m = Markup.parse_int (Future.join promise)
    1.43                handle Fail _ => error "Stopped";
    1.44            in
    1.45 -            Synchronized.change command_tracing_messages
    1.46 +            Synchronized.change tracing_messages
    1.47                (Inttab.map_default (id, 0) (fn k => k - m))
    1.48            end
    1.49        end);
    1.50 @@ -243,8 +240,7 @@
    1.51          if Multithreading.max_threads_value () < 2
    1.52          then Multithreading.max_threads := 2 else ();
    1.53          Goal.skip_proofs := Options.bool options "editor_skip_proofs";
    1.54 -        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
    1.55 -        tracing_messages := Options.int options "editor_tracing_messages"
    1.56 +        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
    1.57        end);
    1.58  
    1.59  end;