# HG changeset patch
# User wenzelm
# Date 1365534840 -7200
# Node ID cba83c9f72b96115c02b8b5eaa3171de35f7d7f2
# Parent  080ef458f21ae39048e2e93a4bfb035581dd5339
tuned signature;

diff -r 080ef458f21a -r cba83c9f72b9 src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Tue Apr 09 20:34:15 2013 +0200
+++ b/src/Pure/General/properties.ML	Tue Apr 09 21:14:00 2013 +0200
@@ -12,6 +12,7 @@
   val get: T -> string -> string option
   val put: entry -> T -> T
   val remove: string -> T -> T
+  val seconds: T -> string -> Time.time
 end;
 
 structure Properties: PROPERTIES =
@@ -25,4 +26,9 @@
 fun put entry (props: T) = AList.update (op =) entry props;
 fun remove name (props: T) = AList.delete (op =) name props;
 
+fun seconds props name =
+  (case AList.lookup (op =) props name of
+    NONE => Time.zeroTime
+  | SOME s => Time.fromReal (the_default 0.0 (Real.fromString s)));
+
 end;
diff -r 080ef458f21a -r cba83c9f72b9 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Apr 09 20:34:15 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Apr 09 21:14:00 2013 +0200
@@ -93,7 +93,6 @@
   val elapsedN: string
   val cpuN: string
   val gcN: string
-  val timing_propertiesN: string list
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   val command_timingN: string
@@ -343,22 +342,18 @@
 val cpuN = "cpu";
 val gcN = "gc";
 
-val timing_propertiesN = [elapsedN, cpuN, gcN];
-
 fun timing_properties {elapsed, cpu, gc} =
  [(elapsedN, Time.toString elapsed),
   (cpuN, Time.toString cpu),
   (gcN, Time.toString gc)];
 
-fun get_time props name =
-  (case AList.lookup (op =) props name of
-    NONE => Time.zeroTime
-  | SOME s => seconds (the_default 0.0 (Real.fromString s)));
+fun parse_timing_properties props =
+ {elapsed = Properties.seconds props elapsedN,
+  cpu = Properties.seconds props cpuN,
+  gc = Properties.seconds props gcN};
 
-fun parse_timing_properties props =
- {elapsed = get_time props elapsedN,
-  cpu = get_time props cpuN,
-  gc = get_time props gcN};
+val timingN = "timing";
+fun timing t = (timingN, timing_properties t);
 
 
 (* command timing *)
@@ -372,16 +367,11 @@
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
-      SOME ({file = file, offset = parse_int offset, name = name}, get_time props elapsedN)
+      SOME ({file = file, offset = parse_int offset, name = name},
+        Properties.seconds props elapsedN)
   | _ => NONE);
 
 
-(* session timing *)
-
-val timingN = "timing";
-fun timing t = (timingN, timing_properties t);
-
-
 (* toplevel *)
 
 val subgoalsN = "subgoals";