# HG changeset patch
# User wenzelm
# Date 1358850534 -3600
# Node ID 890f502f0e895496bec7a7f26e13728383bfd9de
# Parent  bf5f6affa87d24d8d56dacd988552596b636a7af
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);

diff -r bf5f6affa87d -r 890f502f0e89 etc/options
--- a/etc/options	Mon Jan 21 16:50:43 2013 +0100
+++ b/etc/options	Tue Jan 22 11:28:54 2013 +0100
@@ -94,7 +94,7 @@
 option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
-option editor_tracing_messages : int = 100
+option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction"
 
 option editor_chart_delay : real = 3.0
diff -r bf5f6affa87d -r 890f502f0e89 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Jan 21 16:50:43 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Jan 22 11:28:54 2013 +0100
@@ -91,7 +91,7 @@
             val (text, promise) = Active.dialog_text ();
             val _ =
               writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
-                text "10" ^ ", " ^ text "100" ^ ", " ^ text "1000" ^ " messages?")
+                text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
             val m = Markup.parse_int (Future.join promise)
               handle Fail _ => error "Stopped";
           in