smarter handling of tracing messages;
authorwenzelm
Fri Sep 28 16:51:58 2012 +0200 (2012-09-28)
changeset 4964721ae8500d261
parent 49646 77a0a53caa2f
child 49648 e5c16ccc5a87
smarter handling of tracing messages;
NEWS
src/Pure/General/output.ML
src/Pure/Isar/runtime.ML
src/Pure/PIDE/protocol.ML
src/Pure/System/isabelle_process.ML
src/Tools/jEdit/src/output_dockable.scala
     1.1 --- a/NEWS	Fri Sep 28 15:45:03 2012 +0200
     1.2 +++ b/NEWS	Fri Sep 28 16:51:58 2012 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4      . more efficient painting, improved reactivity;
     1.5      . more robust incremental parsing of outer syntax (partial
     1.6        comments, malformed symbols);
     1.7 +    . smarter handling of tracing messages (via tracing_limit);
     1.8      . more plugin options and preferences, based on Isabelle/Scala;
     1.9      . uniform Java 7 platform on Linux, Mac OS X, Windows;
    1.10  
     2.1 --- a/src/Pure/General/output.ML	Fri Sep 28 15:45:03 2012 +0200
     2.2 +++ b/src/Pure/General/output.ML	Fri Sep 28 16:51:58 2012 +0200
     2.3 @@ -43,6 +43,7 @@
     2.4    val status: string -> unit
     2.5    val report: string -> unit
     2.6    val protocol_message: Properties.T -> string -> unit
     2.7 +  exception TRACING_LIMIT of int
     2.8  end;
     2.9  
    2.10  structure Output: OUTPUT =
    2.11 @@ -111,6 +112,8 @@
    2.12  fun report s = ! Private_Hooks.report_fn (output s);
    2.13  fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
    2.14  
    2.15 +exception TRACING_LIMIT of int;
    2.16 +
    2.17  end;
    2.18  
    2.19  structure Basic_Output: BASIC_OUTPUT = Output;
     3.1 --- a/src/Pure/Isar/runtime.ML	Fri Sep 28 15:45:03 2012 +0200
     3.2 +++ b/src/Pure/Isar/runtime.ML	Fri Sep 28 16:51:58 2012 +0200
     3.3 @@ -76,6 +76,7 @@
     3.4              | TOPLEVEL_ERROR => "Error"
     3.5              | ERROR msg => msg
     3.6              | Fail msg => raised exn "Fail" [msg]
     3.7 +            | Output.TRACING_LIMIT n => "Tracing limit exceeded: " ^ string_of_int n
     3.8              | THEORY (msg, thys) =>
     3.9                  raised exn "THEORY" (msg :: map Context.str_of_thy thys)
    3.10              | Ast.AST (msg, asts) =>
     4.1 --- a/src/Pure/PIDE/protocol.ML	Fri Sep 28 15:45:03 2012 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Sep 28 16:51:58 2012 +0200
     4.3 @@ -60,6 +60,7 @@
     4.4                |> YXML.string_of_body);
     4.5  
     4.6          val _ = Goal.cancel_futures ();
     4.7 +        val _ = Isabelle_Process.reset_tracing_limits ();
     4.8          val _ = Document.start_execution state';
     4.9        in state' end));
    4.10  
     5.1 --- a/src/Pure/System/isabelle_process.ML	Fri Sep 28 15:45:03 2012 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Sep 28 16:51:58 2012 +0200
     5.3 @@ -17,6 +17,8 @@
     5.4  sig
     5.5    val is_active: unit -> bool
     5.6    val protocol_command: string -> (string list -> unit) -> unit
     5.7 +  val tracing_limit: int Unsynchronized.ref;
     5.8 +  val reset_tracing_limits: unit -> unit
     5.9    val crashes: exn list Synchronized.var
    5.10    val init_fifos: string -> string -> unit
    5.11    val init_socket: string -> unit
    5.12 @@ -61,6 +63,26 @@
    5.13  end;
    5.14  
    5.15  
    5.16 +(* tracing limit *)
    5.17 +
    5.18 +val tracing_limit = Unsynchronized.ref 500000;
    5.19 +
    5.20 +val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table);
    5.21 +
    5.22 +fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty);
    5.23 +
    5.24 +fun update_tracing_limits msg =
    5.25 +  (case Position.get_id (Position.thread_data ()) of
    5.26 +    NONE => ()
    5.27 +  | SOME id =>
    5.28 +      Synchronized.change tracing_limits (fn tab =>
    5.29 +        let
    5.30 +          val i = Markup.parse_int id;
    5.31 +          val n = the_default 0 (Inttab.lookup tab i) + size msg;
    5.32 +          val _ = if n > ! tracing_limit then raise Output.TRACING_LIMIT n else ();
    5.33 +        in Inttab.update (i, n) tab end));
    5.34 +
    5.35 +
    5.36  (* message channels *)
    5.37  
    5.38  local
    5.39 @@ -105,7 +127,8 @@
    5.40      Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    5.41      Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    5.42      Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
    5.43 -    Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
    5.44 +    Output.Private_Hooks.tracing_fn :=
    5.45 +      (fn s => (update_tracing_limits s; standard_message mbox (SOME (serial ())) "E" s));
    5.46      Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    5.47      Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    5.48      Output.Private_Hooks.protocol_message_fn := message true mbox "H";
     6.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 28 15:45:03 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 28 16:51:58 2012 +0200
     6.3 @@ -76,7 +76,7 @@
     6.4        {
     6.5          val new_output =
     6.6            new_state.results.iterator.map(_._2)
     6.7 -            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
     6.8 +            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList
     6.9          val new_tracing =
    6.10            new_state.results.iterator.map(_._2).filter(Protocol.is_tracing(_)).length
    6.11          (new_output, new_tracing)
    6.12 @@ -149,9 +149,7 @@
    6.13    private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    6.14    zoom.tooltip = "Zoom factor for basic font size"
    6.15  
    6.16 -  private def tracing_text(n: Int): String =
    6.17 -    if (n == 0) "Tracing" else "Tracing (" + n.toString + ")"
    6.18 -
    6.19 +  private def tracing_text(n: Int): String = "Tracing (" + n.toString + ")"
    6.20    private val tracing = new CheckBox(tracing_text(current_tracing)) {
    6.21      reactions += {
    6.22        case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }