smarter handling of tracing messages: prover process pauses and enters user dialog;

--- a/NEWS	Thu Dec 13 18:15:53 2012 +0100
+++ b/NEWS	Thu Dec 13 19:53:55 2012 +0100
@@ -69,10 +69,9 @@
 * More efficient painting and improved reactivity when editing large
 files.  More scalable management of formal document content.
 
-* Smarter handling of tracing messages: output window informs about
-accumulated messages; prover transactions are limited to emit maximum
-amount of output, before being canceled (cf. system option
-"editor_tracing_limit_MB").  This avoids swamping the front-end with
+* Smarter handling of tracing messages: prover process pauses after
+certain number of messages per command transaction, with some user
+dialog to stop or continue.  This avoids swamping the front-end with
 potentially infinite message streams.
 
 * More plugin options and preferences, based on Isabelle/Scala.  The

--- a/etc/options	Thu Dec 13 18:15:53 2012 +0100
+++ b/etc/options	Thu Dec 13 19:53:55 2012 +0100
@@ -96,5 +96,5 @@
 option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
-option editor_tracing_limit_MB : real = 2.5
-  -- "maximum tracing volume for each command transaction"
+option editor_tracing_messages : int = 100
+  -- "initial number of tracing messages for each command transaction"

--- a/src/Pure/General/output.ML	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/General/output.ML	Thu Dec 13 19:53:55 2012 +0100
@@ -45,7 +45,6 @@
   val report: string -> unit
   val result: serial * string -> unit
   val protocol_message: Properties.T -> string -> unit
-  exception TRACING_LIMIT of int
 end;
 
 structure Output: OUTPUT =
@@ -116,8 +115,6 @@
 fun result (i, s) = ! Private_Hooks.result_fn (i, 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	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/Isar/runtime.ML	Thu Dec 13 19:53:55 2012 +0100
@@ -76,7 +76,6 @@
             | 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/active.ML	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/PIDE/active.ML	Thu Dec 13 19:53:55 2012 +0100
@@ -12,6 +12,7 @@
   val sendback_markup_implicit: string -> string
   val sendback_markup: string -> string
   val dialog: unit -> (string -> Markup.T) * string future
+  val dialog_text: unit -> (string -> string) * string future
   val dialog_result: serial -> string -> unit
 end;
 
@@ -53,6 +54,10 @@
     fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
   in (result_markup, promise) end;
 
+fun dialog_text () =
+  let val (markup, promise) = dialog ()
+  in (fn s => Markup.markup (markup s) s, promise) end;
+
 fun dialog_result i result =
   Synchronized.change_result dialogs
     (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))

--- a/src/Pure/PIDE/protocol.ML	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Dec 13 19:53:55 2012 +0100
@@ -60,7 +60,7 @@
               |> YXML.string_of_body);
 
         val _ = List.app Future.cancel_group (Goal.reset_futures ());
-        val _ = Isabelle_Process.reset_tracing_limits ();
+        val _ = Isabelle_Process.reset_tracing ();
         val _ = Document.start_execution state';
       in state' end));
 

--- a/src/Pure/System/isabelle_process.ML	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Dec 13 19:53:55 2012 +0100
@@ -17,8 +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 tracing_messages: int Unsynchronized.ref;
+  val reset_tracing: unit -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
   val init_socket: string -> unit
@@ -63,24 +63,43 @@
 end;
 
 
-(* tracing limit *)
+(* restricted tracing messages *)
 
-val tracing_limit = Unsynchronized.ref 1000000;
+val tracing_messages = Unsynchronized.ref 100;
 
-val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
+val command_tracing_messages =
+  Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table);
 
-fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
+fun reset_tracing () =
+  Synchronized.change command_tracing_messages (K Inttab.empty);
 
-fun update_tracing_limits msg =
+fun update_tracing () =
   (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));
+      let
+        val i = Markup.parse_int id;
+        val (n, ok) =
+          Synchronized.change_result command_tracing_messages (fn tab =>
+            let
+              val n = the_default 0 (Inttab.lookup tab i) + 1;
+              val ok = n <= ! tracing_messages;
+            in ((n, ok), Inttab.update (i, n) tab) end);
+      in
+        if ok then ()
+        else
+          let
+            val (text, promise) = Active.dialog_text ();
+            val _ =
+              writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
+                text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?")
+            val m = Markup.parse_int (Future.join promise)
+              handle Fail _ => error "Stopped";
+          in
+            Synchronized.change command_tracing_messages
+              (Inttab.map_default (i, 0) (fn k => k - m))
+          end
+      end);
 
 
 (* message channels *)
@@ -131,7 +150,7 @@
     Output.Private_Hooks.writeln_fn :=
       (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
     Output.Private_Hooks.tracing_fn :=
-      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
+      (fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s));
     Output.Private_Hooks.warning_fn :=
       (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
     Output.Private_Hooks.error_fn :=
@@ -226,8 +245,7 @@
         then Multithreading.max_threads := 2 else ();
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
         Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
-        tracing_limit :=
-          Real.round (Options.real options "editor_tracing_limit_MB" * 1024.0 * 1024.0)
+        tracing_messages := Options.int options "editor_tracing_messages"
       end);
 
 end;

--- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Dec 13 18:15:53 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Dec 13 19:53:55 2012 +0100
@@ -45,7 +45,7 @@
       "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
       "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
       "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
-      "editor_tracing_limit_MB", "editor_update_delay")
+      "editor_tracing_messages", "editor_update_delay")
 
   relevant_options.foreach(PIDE.options.value.check_name _)