# 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 => ())