more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
authorwenzelm
Tue Jan 22 11:28:54 2013 +0100 (2013-01-22)
changeset 51044890f502f0e89
parent 51043 bf5f6affa87d
child 51045 630c0895d9d1
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
etc/options
src/Pure/System/isabelle_process.ML
     1.1 --- a/etc/options	Mon Jan 21 16:50:43 2013 +0100
     1.2 +++ b/etc/options	Tue Jan 22 11:28:54 2013 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4  option editor_reparse_limit : int = 10000
     1.5    -- "maximum amount of reparsed text outside perspective"
     1.6  
     1.7 -option editor_tracing_messages : int = 100
     1.8 +option editor_tracing_messages : int = 1000
     1.9    -- "initial number of tracing messages for each command transaction"
    1.10  
    1.11  option editor_chart_delay : real = 3.0
     2.1 --- a/src/Pure/System/isabelle_process.ML	Mon Jan 21 16:50:43 2013 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jan 22 11:28:54 2013 +0100
     2.3 @@ -91,7 +91,7 @@
     2.4              val (text, promise) = Active.dialog_text ();
     2.5              val _ =
     2.6                writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
     2.7 -                text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?")
     2.8 +                text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
     2.9              val m = Markup.parse_int (Future.join promise)
    2.10                handle Fail _ => error "Stopped";
    2.11            in