# HG changeset patch # User wenzelm # Date 1459522818 -7200 # Node ID f235646b1b7380c04851098beb42590bfb5dd227 # Parent 340428bebdb832eb9d7255ff60bcf4425be3938b less bulky timing information, e.g. HOL 56913 ~> 672; diff -r 340428bebdb8 -r f235646b1b73 etc/options --- a/etc/options Fri Apr 01 16:32:20 2016 +0200 +++ b/etc/options Fri Apr 01 17:00:18 2016 +0200 @@ -76,6 +76,9 @@ option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" +option command_timing_threshold : real = 0.1 + -- "default threshold for persistent command timing (seconds)" + section "Detail of Proof Checking" diff -r 340428bebdb8 -r f235646b1b73 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Fri Apr 01 16:32:20 2016 +0200 +++ b/src/Pure/Tools/build.ML Fri Apr 01 17:00:18 2016 +0200 @@ -81,8 +81,11 @@ val name = the_default "" (Properties.get args Markup.nameN); val pos = Position.of_properties args; val {elapsed, ...} = Markup.parse_timing_properties args; + val is_significant = + Timing.is_relevant_time elapsed andalso + Time.>= (elapsed, Options.default_seconds "command_timing_threshold"); in - if Timing.is_relevant_time elapsed then + if is_significant then (case approximative_id name pos of SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed) | NONE => ())