# HG changeset patch # User wenzelm # Date 1355424835 -3600 # Node ID 33c92722cc3d9ef83a81fbd3c1c120e308c39acf # Parent 2cc6eab90cdf3e387eb90b6e89ba19d131ce687f smarter handling of tracing messages: prover process pauses and enters user dialog; diff -r 2cc6eab90cdf -r 33c92722cc3d NEWS --- 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 diff -r 2cc6eab90cdf -r 33c92722cc3d etc/options --- 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" diff -r 2cc6eab90cdf -r 33c92722cc3d src/Pure/General/output.ML --- 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; diff -r 2cc6eab90cdf -r 33c92722cc3d src/Pure/Isar/runtime.ML --- 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) => diff -r 2cc6eab90cdf -r 33c92722cc3d src/Pure/PIDE/active.ML --- 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)) diff -r 2cc6eab90cdf -r 33c92722cc3d src/Pure/PIDE/protocol.ML --- 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)); diff -r 2cc6eab90cdf -r 33c92722cc3d src/Pure/System/isabelle_process.ML --- 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; diff -r 2cc6eab90cdf -r 33c92722cc3d src/Tools/jEdit/src/isabelle_options.scala --- 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 _)