# HG changeset patch # User wenzelm # Date 1538499767 -7200 # Node ID 814a1ab42d70e815013f31d2c81adb9625a3fe0c # Parent 4b06a20b13b54400d8ebb055c4aa55b129c85e19 unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers; diff -r 4b06a20b13b5 -r 814a1ab42d70 etc/options --- a/etc/options Mon Oct 01 19:30:36 2018 +0200 +++ b/etc/options Tue Oct 02 19:02:47 2018 +0200 @@ -174,7 +174,7 @@ -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 - -- "initial number of tracing messages for each command transaction" + -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" diff -r 4b06a20b13b5 -r 814a1ab42d70 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Mon Oct 01 19:30:36 2018 +0200 +++ b/src/Pure/System/isabelle_process.ML Tue Oct 02 19:02:47 2018 +0200 @@ -71,7 +71,8 @@ Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; - val ok = n <= Options.default_int "editor_tracing_messages"; + val limit = Options.default_int "editor_tracing_messages"; + val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () diff -r 4b06a20b13b5 -r 814a1ab42d70 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Mon Oct 01 19:30:36 2018 +0200 +++ b/src/Pure/Tools/dump.scala Tue Oct 02 19:02:47 2018 +0200 @@ -80,7 +80,9 @@ def make_options(options: Options, aspects: List[Aspect]): Options = { val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options - val options1 = options0 + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0" + val options1 = + options0 + "completion_limit=0" + "ML_statistics=false" + + "parallel_proofs=0" + "editor_tracing_messages=0" (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) }