# 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