smarter handling of tracing messages: prover process pauses and enters user dialog;
authorwenzelm
Thu Dec 13 19:53:55 2012 +0100 (2012-12-13)
changeset 5050533c92722cc3d
parent 50504 2cc6eab90cdf
child 50506 7d8406ebe18f
child 50507 9605b0d93d1e
smarter handling of tracing messages: prover process pauses and enters user dialog;
NEWS
etc/options
src/Pure/General/output.ML
src/Pure/Isar/runtime.ML
src/Pure/PIDE/active.ML
src/Pure/PIDE/protocol.ML
src/Pure/System/isabelle_process.ML
src/Tools/jEdit/src/isabelle_options.scala
     1.1 --- a/NEWS	Thu Dec 13 18:15:53 2012 +0100
     1.2 +++ b/NEWS	Thu Dec 13 19:53:55 2012 +0100
     1.3 @@ -69,10 +69,9 @@
     1.4  * More efficient painting and improved reactivity when editing large
     1.5  files.  More scalable management of formal document content.
     1.6  
     1.7 -* Smarter handling of tracing messages: output window informs about
     1.8 -accumulated messages; prover transactions are limited to emit maximum
     1.9 -amount of output, before being canceled (cf. system option
    1.10 -"editor_tracing_limit_MB").  This avoids swamping the front-end with
    1.11 +* Smarter handling of tracing messages: prover process pauses after
    1.12 +certain number of messages per command transaction, with some user
    1.13 +dialog to stop or continue.  This avoids swamping the front-end with
    1.14  potentially infinite message streams.
    1.15  
    1.16  * More plugin options and preferences, based on Isabelle/Scala.  The
     2.1 --- a/etc/options	Thu Dec 13 18:15:53 2012 +0100
     2.2 +++ b/etc/options	Thu Dec 13 19:53:55 2012 +0100
     2.3 @@ -96,5 +96,5 @@
     2.4  option editor_reparse_limit : int = 10000
     2.5    -- "maximum amount of reparsed text outside perspective"
     2.6  
     2.7 -option editor_tracing_limit_MB : real = 2.5
     2.8 -  -- "maximum tracing volume for each command transaction"
     2.9 +option editor_tracing_messages : int = 100
    2.10 +  -- "initial number of tracing messages for each command transaction"
     3.1 --- a/src/Pure/General/output.ML	Thu Dec 13 18:15:53 2012 +0100
     3.2 +++ b/src/Pure/General/output.ML	Thu Dec 13 19:53:55 2012 +0100
     3.3 @@ -45,7 +45,6 @@
     3.4    val report: string -> unit
     3.5    val result: serial * string -> unit
     3.6    val protocol_message: Properties.T -> string -> unit
     3.7 -  exception TRACING_LIMIT of int
     3.8  end;
     3.9  
    3.10  structure Output: OUTPUT =
    3.11 @@ -116,8 +115,6 @@
    3.12  fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
    3.13  fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
    3.14  
    3.15 -exception TRACING_LIMIT of int;
    3.16 -
    3.17  end;
    3.18  
    3.19  structure Basic_Output: BASIC_OUTPUT = Output;
     4.1 --- a/src/Pure/Isar/runtime.ML	Thu Dec 13 18:15:53 2012 +0100
     4.2 +++ b/src/Pure/Isar/runtime.ML	Thu Dec 13 19:53:55 2012 +0100
     4.3 @@ -76,7 +76,6 @@
     4.4              | TOPLEVEL_ERROR => "Error"
     4.5              | ERROR msg => msg
     4.6              | Fail msg => raised exn "Fail" [msg]
     4.7 -            | Output.TRACING_LIMIT n => "Tracing limit exceeded: " ^ string_of_int n
     4.8              | THEORY (msg, thys) =>
     4.9                  raised exn "THEORY" (msg :: map Context.str_of_thy thys)
    4.10              | Ast.AST (msg, asts) =>
     5.1 --- a/src/Pure/PIDE/active.ML	Thu Dec 13 18:15:53 2012 +0100
     5.2 +++ b/src/Pure/PIDE/active.ML	Thu Dec 13 19:53:55 2012 +0100
     5.3 @@ -12,6 +12,7 @@
     5.4    val sendback_markup_implicit: string -> string
     5.5    val sendback_markup: string -> string
     5.6    val dialog: unit -> (string -> Markup.T) * string future
     5.7 +  val dialog_text: unit -> (string -> string) * string future
     5.8    val dialog_result: serial -> string -> unit
     5.9  end;
    5.10  
    5.11 @@ -53,6 +54,10 @@
    5.12      fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
    5.13    in (result_markup, promise) end;
    5.14  
    5.15 +fun dialog_text () =
    5.16 +  let val (markup, promise) = dialog ()
    5.17 +  in (fn s => Markup.markup (markup s) s, promise) end;
    5.18 +
    5.19  fun dialog_result i result =
    5.20    Synchronized.change_result dialogs
    5.21      (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
     6.1 --- a/src/Pure/PIDE/protocol.ML	Thu Dec 13 18:15:53 2012 +0100
     6.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Dec 13 19:53:55 2012 +0100
     6.3 @@ -60,7 +60,7 @@
     6.4                |> YXML.string_of_body);
     6.5  
     6.6          val _ = List.app Future.cancel_group (Goal.reset_futures ());
     6.7 -        val _ = Isabelle_Process.reset_tracing_limits ();
     6.8 +        val _ = Isabelle_Process.reset_tracing ();
     6.9          val _ = Document.start_execution state';
    6.10        in state' end));
    6.11  
     7.1 --- a/src/Pure/System/isabelle_process.ML	Thu Dec 13 18:15:53 2012 +0100
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Dec 13 19:53:55 2012 +0100
     7.3 @@ -17,8 +17,8 @@
     7.4  sig
     7.5    val is_active: unit -> bool
     7.6    val protocol_command: string -> (string list -> unit) -> unit
     7.7 -  val tracing_limit: int Unsynchronized.ref;
     7.8 -  val reset_tracing_limits: unit -> unit
     7.9 +  val tracing_messages: int Unsynchronized.ref;
    7.10 +  val reset_tracing: unit -> unit
    7.11    val crashes: exn list Synchronized.var
    7.12    val init_fifos: string -> string -> unit
    7.13    val init_socket: string -> unit
    7.14 @@ -63,24 +63,43 @@
    7.15  end;
    7.16  
    7.17  
    7.18 -(* tracing limit *)
    7.19 +(* restricted tracing messages *)
    7.20  
    7.21 -val tracing_limit = Unsynchronized.ref 1000000;
    7.22 +val tracing_messages = Unsynchronized.ref 100;
    7.23  
    7.24 -val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
    7.25 +val command_tracing_messages =
    7.26 +  Synchronized.var "command_tracing_messages" (Inttab.empty: int Inttab.table);
    7.27  
    7.28 -fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
    7.29 +fun reset_tracing () =
    7.30 +  Synchronized.change command_tracing_messages (K Inttab.empty);
    7.31  
    7.32 -fun update_tracing_limits msg =
    7.33 +fun update_tracing () =
    7.34    (case Position.get_id (Position.thread_data ()) of
    7.35      NONE => ()
    7.36    | SOME id =>
    7.37 -      Synchronized.change tracing_limits (fn tab =>
    7.38 -        let
    7.39 -          val i = Markup.parse_int id;
    7.40 -          val n = the_default 0 (Inttab.lookup tab i) + size msg;
    7.41 -          val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
    7.42 -        in Inttab.update (i, n) tab end));
    7.43 +      let
    7.44 +        val i = Markup.parse_int id;
    7.45 +        val (n, ok) =
    7.46 +          Synchronized.change_result command_tracing_messages (fn tab =>
    7.47 +            let
    7.48 +              val n = the_default 0 (Inttab.lookup tab i) + 1;
    7.49 +              val ok = n <= ! tracing_messages;
    7.50 +            in ((n, ok), Inttab.update (i, n) tab) end);
    7.51 +      in
    7.52 +        if ok then ()
    7.53 +        else
    7.54 +          let
    7.55 +            val (text, promise) = Active.dialog_text ();
    7.56 +            val _ =
    7.57 +              writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
    7.58 +                text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?")
    7.59 +            val m = Markup.parse_int (Future.join promise)
    7.60 +              handle Fail _ => error "Stopped";
    7.61 +          in
    7.62 +            Synchronized.change command_tracing_messages
    7.63 +              (Inttab.map_default (i, 0) (fn k => k - m))
    7.64 +          end
    7.65 +      end);
    7.66  
    7.67  
    7.68  (* message channels *)
    7.69 @@ -131,7 +150,7 @@
    7.70      Output.Private_Hooks.writeln_fn :=
    7.71        (fn s => standard_message mbox (SOME (serial ())) Markup.writelnN s);
    7.72      Output.Private_Hooks.tracing_fn :=
    7.73 -      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) Markup.tracingN s));
    7.74 +      (fn s => (update_tracing (); standard_message mbox (SOME (serial ())) Markup.tracingN s));
    7.75      Output.Private_Hooks.warning_fn :=
    7.76        (fn s => standard_message mbox (SOME (serial ())) Markup.warningN s);
    7.77      Output.Private_Hooks.error_fn :=
    7.78 @@ -226,8 +245,7 @@
    7.79          then Multithreading.max_threads := 2 else ();
    7.80          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
    7.81          Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
    7.82 -        tracing_limit :=
    7.83 -          Real.round (Options.real options "editor_tracing_limit_MB" * 1024.0 * 1024.0)
    7.84 +        tracing_messages := Options.int options "editor_tracing_messages"
    7.85        end);
    7.86  
    7.87  end;
     8.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Dec 13 18:15:53 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Dec 13 19:53:55 2012 +0100
     8.3 @@ -45,7 +45,7 @@
     8.4        "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
     8.5        "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
     8.6        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
     8.7 -      "editor_tracing_limit_MB", "editor_update_delay")
     8.8 +      "editor_tracing_messages", "editor_update_delay")
     8.9  
    8.10    relevant_options.foreach(PIDE.options.value.check_name _)
    8.11