more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
authorwenzelm
Sat Nov 04 12:25:09 2017 +0100 (12 months ago)
changeset 670001698e9ccef2d
parent 66999 c70c47dcf63e
child 67001 b34fbf33a7ea
more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;
src/Pure/Concurrent/timeout.ML
src/Pure/General/timing.ML
src/Pure/General/value.ML
src/Pure/PIDE/markup.ML
     1.1 --- a/src/Pure/Concurrent/timeout.ML	Sat Nov 04 11:42:08 2017 +0100
     1.2 +++ b/src/Pure/Concurrent/timeout.ML	Sat Nov 04 12:25:09 2017 +0100
     1.3 @@ -37,6 +37,6 @@
     1.4        else (Exn.release test; Exn.release result)
     1.5      end);
     1.6  
     1.7 -fun print t = "Timeout after " ^ Time.toString t ^ "s";
     1.8 +fun print t = "Timeout after " ^ Value.print_time t ^ "s";
     1.9  
    1.10  end;
     2.1 --- a/src/Pure/General/timing.ML	Sat Nov 04 11:42:08 2017 +0100
     2.2 +++ b/src/Pure/General/timing.ML	Sat Nov 04 12:25:09 2017 +0100
     2.3 @@ -84,9 +84,9 @@
     2.4    is_relevant_time gc;
     2.5  
     2.6  fun message {elapsed, cpu, gc} =
     2.7 -  Time.toString elapsed ^ "s elapsed time, " ^
     2.8 -  Time.toString cpu ^ "s cpu time, " ^
     2.9 -  Time.toString gc ^ "s GC time" handle Time.Time => "";
    2.10 +  Value.print_time elapsed ^ "s elapsed time, " ^
    2.11 +  Value.print_time cpu ^ "s cpu time, " ^
    2.12 +  Value.print_time gc ^ "s GC time" handle Time.Time => "";
    2.13  
    2.14  fun cond_timeit enabled msg e =
    2.15    if enabled then
     3.1 --- a/src/Pure/General/value.ML	Sat Nov 04 11:42:08 2017 +0100
     3.2 +++ b/src/Pure/General/value.ML	Sat Nov 04 12:25:09 2017 +0100
     3.3 @@ -13,11 +13,15 @@
     3.4    val print_int: int -> string
     3.5    val parse_real: string -> real
     3.6    val print_real: real -> string
     3.7 +  val parse_time: string -> Time.time
     3.8 +  val print_time: Time.time -> string
     3.9  end;
    3.10  
    3.11  structure Value: VALUE =
    3.12  struct
    3.13  
    3.14 +(* bool *)
    3.15 +
    3.16  fun parse_bool "true" = true
    3.17    | parse_bool "false" = false
    3.18    | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
    3.19 @@ -25,6 +29,8 @@
    3.20  val print_bool = Bool.toString;
    3.21  
    3.22  
    3.23 +(* nat and int *)
    3.24 +
    3.25  fun parse_nat s =
    3.26    let val i = Int.fromString s in
    3.27      if is_none i orelse the i < 0
    3.28 @@ -42,6 +48,8 @@
    3.29  val print_int = signed_string_of_int;
    3.30  
    3.31  
    3.32 +(* real *)
    3.33 +
    3.34  fun parse_real s =
    3.35    (case Real.fromString s of
    3.36      SOME x => x
    3.37 @@ -54,4 +62,16 @@
    3.38      | _ => s)
    3.39    end;
    3.40  
    3.41 +
    3.42 +(* time *)
    3.43 +
    3.44 +fun parse_time s =
    3.45 +  (case Time.fromString s of
    3.46 +    SOME x => x
    3.47 +  | NONE => raise Fail ("Bad time " ^ quote s));
    3.48 +
    3.49 +fun print_time x =
    3.50 +  if x < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - x)
    3.51 +  else Time.toString x;
    3.52 +
    3.53  end;
     4.1 --- a/src/Pure/PIDE/markup.ML	Sat Nov 04 11:42:08 2017 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sat Nov 04 12:25:09 2017 +0100
     4.3 @@ -507,9 +507,9 @@
     4.4  val gcN = "gc";
     4.5  
     4.6  fun timing_properties {elapsed, cpu, gc} =
     4.7 - [(elapsedN, Time.toString elapsed),
     4.8 -  (cpuN, Time.toString cpu),
     4.9 -  (gcN, Time.toString gc)];
    4.10 + [(elapsedN, Value.print_time elapsed),
    4.11 +  (cpuN, Value.print_time cpu),
    4.12 +  (gcN, Value.print_time gc)];
    4.13  
    4.14  fun parse_timing_properties props =
    4.15   {elapsed = Properties.seconds props elapsedN,
    4.16 @@ -526,7 +526,7 @@
    4.17  
    4.18  fun command_timing_properties {file, offset, name} elapsed =
    4.19   [(fileN, file), (offsetN, Value.print_int offset),
    4.20 -  (nameN, name), (elapsedN, Time.toString elapsed)];
    4.21 +  (nameN, name), (elapsedN, Value.print_time elapsed)];
    4.22  
    4.23  fun parse_command_timing_properties props =
    4.24    (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of