1.1 --- a/src/Pure/System/isabelle_process.ML	Fri Sep 28 15:45:03 2012 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Sep 28 16:51:58 2012 +0200
     1.3 @@ -17,6 +17,8 @@
     1.4  sig
     1.5    val is_active: unit -> bool
     1.6    val protocol_command: string -> (string list -> unit) -> unit
     1.7 +  val tracing_limit: int Unsynchronized.ref;
     1.8 +  val reset_tracing_limits: unit -> 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 @@ -61,6 +63,26 @@
    1.13  end;
    1.14  
    1.15  
    1.16 +(* tracing limit *)
    1.17 +
    1.18 +val tracing_limit = Unsynchronized.ref 500000;
    1.19 +
    1.20 +val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
    1.21 +
    1.22 +fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
    1.23 +
    1.24 +fun update_tracing_limits msg =
    1.25 +  (case Position.get_id (Position.thread_data ()) of
    1.26 +    NONE => ()
    1.27 +  | SOME id =>
    1.28 +      Synchronized.change tracing_limits (fn tab =>
    1.29 +        let
    1.30 +          val i = Markup.parse_int id;
    1.31 +          val n = the_default 0 (Inttab.lookup tab i) + size msg;
    1.32 +          val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
    1.33 +        in Inttab.update (i, n) tab end));
    1.34 +
    1.35 +
    1.36  (* message channels *)
    1.37  
    1.38  local
    1.39 @@ -105,7 +127,8 @@
    1.40      Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    1.41      Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    1.42      Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
    1.43 -    Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
    1.44 +    Output.Private_Hooks.tracing_fn :=
    1.45 +      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
    1.46      Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    1.47      Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    1.48      Output.Private_Hooks.protocol_message_fn := message true mbox "H";