--- a/src/Pure/Concurrent/task_queue.ML Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Tue May 14 20:46:09 2013 +0200
@@ -153,7 +153,7 @@
(case timing of NONE => timing_start | SOME var => Synchronized.value var);
fun micros time = string_of_int (Time.toNanoseconds time div 1000);
in
- [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+ [("now", Markup.print_real (Time.toReal (Time.now ()))),
("task_name", name), ("task_id", Markup.print_int id),
("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
Position.properties_of pos