src/Pure/System/isabelle_process.ML

--- a/src/Pure/System/isabelle_process.ML	Fri Sep 28 15:45:03 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Sep 28 16:51:58 2012 +0200
@@ -17,6 +17,8 @@
 sig
   val is_active: unit -> bool
   val protocol_command: string -> (string list -> unit) -> unit
+  val tracing_limit: int Unsynchronized.ref;
+  val reset_tracing_limits: unit -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
   val init_socket: string -> unit
@@ -61,6 +63,26 @@
 end;
 
 
+(* tracing limit *)
+
+val tracing_limit = Unsynchronized.ref 500000;
+
+val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
+
+fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
+
+fun update_tracing_limits msg =
+  (case Position.get_id (Position.thread_data ()) of
+    NONE => ()
+  | SOME id =>
+      Synchronized.change tracing_limits (fn tab =>
+        let
+          val i = Markup.parse_int id;
+          val n = the_default 0 (Inttab.lookup tab i) + size msg;
+          val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
+        in Inttab.update (i, n) tab end));
+
+
 (* message channels *)
 
 local
@@ -105,7 +127,8 @@
     Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
     Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
     Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
-    Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
+    Output.Private_Hooks.tracing_fn :=
+      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
     Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
     Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
     Output.Private_Hooks.protocol_message_fn := message true mbox "H";