# HG changeset patch # User wenzelm # Date 1509794709 -3600 # Node ID 1698e9ccef2d92373b19309cf05c0657c55f4dde # Parent c70c47dcf63e4be07cb120c805aa0dd6dd844fe0 more portable print_time, notably for occasional negative (!) elapsed time of theory_timing; diff -r c70c47dcf63e -r 1698e9ccef2d src/Pure/Concurrent/timeout.ML --- a/src/Pure/Concurrent/timeout.ML Sat Nov 04 11:42:08 2017 +0100 +++ b/src/Pure/Concurrent/timeout.ML Sat Nov 04 12:25:09 2017 +0100 @@ -37,6 +37,6 @@ else (Exn.release test; Exn.release result) end); -fun print t = "Timeout after " ^ Time.toString t ^ "s"; +fun print t = "Timeout after " ^ Value.print_time t ^ "s"; end; diff -r c70c47dcf63e -r 1698e9ccef2d src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Sat Nov 04 11:42:08 2017 +0100 +++ b/src/Pure/General/timing.ML Sat Nov 04 12:25:09 2017 +0100 @@ -84,9 +84,9 @@ is_relevant_time gc; fun message {elapsed, cpu, gc} = - Time.toString elapsed ^ "s elapsed time, " ^ - Time.toString cpu ^ "s cpu time, " ^ - Time.toString gc ^ "s GC time" handle Time.Time => ""; + Value.print_time elapsed ^ "s elapsed time, " ^ + Value.print_time cpu ^ "s cpu time, " ^ + Value.print_time gc ^ "s GC time" handle Time.Time => ""; fun cond_timeit enabled msg e = if enabled then diff -r c70c47dcf63e -r 1698e9ccef2d src/Pure/General/value.ML --- a/src/Pure/General/value.ML Sat Nov 04 11:42:08 2017 +0100 +++ b/src/Pure/General/value.ML Sat Nov 04 12:25:09 2017 +0100 @@ -13,11 +13,15 @@ val print_int: int -> string val parse_real: string -> real val print_real: real -> string + val parse_time: string -> Time.time + val print_time: Time.time -> string end; structure Value: VALUE = struct +(* bool *) + fun parse_bool "true" = true | parse_bool "false" = false | parse_bool s = raise Fail ("Bad boolean " ^ quote s); @@ -25,6 +29,8 @@ val print_bool = Bool.toString; +(* nat and int *) + fun parse_nat s = let val i = Int.fromString s in if is_none i orelse the i < 0 @@ -42,6 +48,8 @@ val print_int = signed_string_of_int; +(* real *) + fun parse_real s = (case Real.fromString s of SOME x => x @@ -54,4 +62,16 @@ | _ => s) end; + +(* time *) + +fun parse_time s = + (case Time.fromString s of + SOME x => x + | NONE => raise Fail ("Bad time " ^ quote s)); + +fun print_time x = + if x < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - x) + else Time.toString x; + end; diff -r c70c47dcf63e -r 1698e9ccef2d src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Nov 04 11:42:08 2017 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Nov 04 12:25:09 2017 +0100 @@ -507,9 +507,9 @@ val gcN = "gc"; fun timing_properties {elapsed, cpu, gc} = - [(elapsedN, Time.toString elapsed), - (cpuN, Time.toString cpu), - (gcN, Time.toString gc)]; + [(elapsedN, Value.print_time elapsed), + (cpuN, Value.print_time cpu), + (gcN, Value.print_time gc)]; fun parse_timing_properties props = {elapsed = Properties.seconds props elapsedN, @@ -526,7 +526,7 @@ fun command_timing_properties {file, offset, name} elapsed = [(fileN, file), (offsetN, Value.print_int offset), - (nameN, name), (elapsedN, Time.toString elapsed)]; + (nameN, name), (elapsedN, Value.print_time elapsed)]; fun parse_command_timing_properties props = (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of