smarter handling of tracing messages;

--- a/NEWS	Fri Sep 28 15:45:03 2012 +0200
+++ b/NEWS	Fri Sep 28 16:51:58 2012 +0200
@@ -12,6 +12,7 @@
     . more efficient painting, improved reactivity;
     . more robust incremental parsing of outer syntax (partial
       comments, malformed symbols);
+    . smarter handling of tracing messages (via tracing_limit);
     . more plugin options and preferences, based on Isabelle/Scala;
     . uniform Java 7 platform on Linux, Mac OS X, Windows;
 

--- a/src/Pure/General/output.ML	Fri Sep 28 15:45:03 2012 +0200
+++ b/src/Pure/General/output.ML	Fri Sep 28 16:51:58 2012 +0200
@@ -43,6 +43,7 @@
   val status: string -> unit
   val report: string -> unit
   val protocol_message: Properties.T -> string -> unit
+  exception TRACING_LIMIT of int
 end;
 
 structure Output: OUTPUT =
@@ -111,6 +112,8 @@
 fun report s = ! Private_Hooks.report_fn (output s);
 fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
 
+exception TRACING_LIMIT of int;
+
 end;
 
 structure Basic_Output: BASIC_OUTPUT = Output;

--- a/src/Pure/Isar/runtime.ML	Fri Sep 28 15:45:03 2012 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Sep 28 16:51:58 2012 +0200
@@ -76,6 +76,7 @@
             | TOPLEVEL_ERROR => "Error"
             | ERROR msg => msg
             | Fail msg => raised exn "Fail" [msg]
+            | Output.TRACING_LIMIT n => "Tracing limit exceeded: " ^ string_of_int n
             | THEORY (msg, thys) =>
                 raised exn "THEORY" (msg :: map Context.str_of_thy thys)
             | Ast.AST (msg, asts) =>

--- a/src/Pure/PIDE/protocol.ML	Fri Sep 28 15:45:03 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Sep 28 16:51:58 2012 +0200
@@ -60,6 +60,7 @@
               |> YXML.string_of_body);
 
         val _ = Goal.cancel_futures ();
+        val _ = Isabelle_Process.reset_tracing_limits ();
         val _ = Document.start_execution state';
       in state' end));
 

--- 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";

--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 28 15:45:03 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 28 16:51:58 2012 +0200
@@ -76,7 +76,7 @@
       {
         val new_output =
           new_state.results.iterator.map(_._2)
-            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
+            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList
         val new_tracing =
           new_state.results.iterator.map(_._2).filter(Protocol.is_tracing(_)).length
         (new_output, new_tracing)
@@ -149,9 +149,7 @@
   private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   zoom.tooltip = "Zoom factor for basic font size"
 
-  private def tracing_text(n: Int): String =
-    if (n == 0) "Tracing" else "Tracing (" + n.toString + ")"
-
+  private def tracing_text(n: Int): String = "Tracing (" + n.toString + ")"
   private val tracing = new CheckBox(tracing_text(current_tracing)) {
     reactions += {
       case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }