less bulky timing information, e.g. HOL 56913 ~> 672;
authorwenzelm
Fri Apr 01 17:00:18 2016 +0200 (2016-04-01)
changeset 62793f235646b1b73
parent 62792 340428bebdb8
child 62794 c4fa2b381591
less bulky timing information, e.g. HOL 56913 ~> 672;
etc/options
src/Pure/Tools/build.ML
     1.1 --- a/etc/options	Fri Apr 01 16:32:20 2016 +0200
     1.2 +++ b/etc/options	Fri Apr 01 17:00:18 2016 +0200
     1.3 @@ -76,6 +76,9 @@
     1.4  option parallel_subproofs_threshold : real = 0.01
     1.5    -- "lower bound of timing estimate for forked nested proofs (seconds)"
     1.6  
     1.7 +option command_timing_threshold : real = 0.1
     1.8 +  -- "default threshold for persistent command timing (seconds)"
     1.9 +
    1.10  
    1.11  section "Detail of Proof Checking"
    1.12  
     2.1 --- a/src/Pure/Tools/build.ML	Fri Apr 01 16:32:20 2016 +0200
     2.2 +++ b/src/Pure/Tools/build.ML	Fri Apr 01 17:00:18 2016 +0200
     2.3 @@ -81,8 +81,11 @@
     2.4            val name = the_default "" (Properties.get args Markup.nameN);
     2.5            val pos = Position.of_properties args;
     2.6            val {elapsed, ...} = Markup.parse_timing_properties args;
     2.7 +          val is_significant =
     2.8 +            Timing.is_relevant_time elapsed andalso
     2.9 +            Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
    2.10          in
    2.11 -          if Timing.is_relevant_time elapsed then
    2.12 +          if is_significant then
    2.13              (case approximative_id name pos of
    2.14                SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    2.15              | NONE => ())