more portable print_time, notably for occasional negative (!) elapsed time of theory_timing;

--- 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;

--- 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

--- 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;

--- 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