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 _)