# HG changeset patch
# User wenzelm
# Date 1322599800 -3600
# Node ID eb65c9d17e2fb1d83d06d33a621b4f9d73849a14
# Parent  cd41e3903fbfa0b0edc0f4cb6b8277d1dc645b1f
clarified Time vs. Timing;

diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/General/time.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/time.scala	Tue Nov 29 21:50:00 2011 +0100
@@ -0,0 +1,28 @@
+/*  Title:      Pure/General/time.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Time based on milliseconds.
+*/
+
+package isabelle
+
+
+object Time
+{
+  def seconds(s: Double): Time = new Time((s * 1000.0) round)
+  def ms(m: Long): Time = new Time(m)
+}
+
+class Time private(val ms: Long)
+{
+  def seconds: Double = ms / 1000.0
+
+  def min(t: Time): Time = if (ms < t.ms) this else t
+  def max(t: Time): Time = if (ms > t.ms) this else t
+
+  override def toString =
+    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+  def message: String = toString + "s"
+}
+
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/General/timing.scala	Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/timing.scala
-    Module:     PIDE
     Author:     Makarius
 
 Basic support for time measurement.
@@ -8,25 +7,6 @@
 package isabelle
 
 
-object Time
-{
-  def seconds(s: Double): Time = new Time((s * 1000.0) round)
-  def ms(m: Long): Time = new Time(m)
-}
-
-class Time private(val ms: Long)
-{
-  def seconds: Double = ms / 1000.0
-
-  def min(t: Time): Time = if (ms < t.ms) this else t
-  def max(t: Time): Time = if (ms > t.ms) this else t
-
-  override def toString =
-    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
-  def message: String = toString + "s"
-}
-
-
 object Timing
 {
   def timeit[A](message: String)(e: => A) =
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Nov 29 21:50:00 2011 +0100
@@ -308,7 +308,7 @@
 local
 
 fun timing tr t =
-  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
+  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
 
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Nov 29 21:50:00 2011 +0100
@@ -82,6 +82,10 @@
   val ignored_spanN: string val ignored_span: Markup.T
   val malformed_spanN: string val malformed_span: Markup.T
   val loaded_theoryN: string val loaded_theory: string -> Markup.T
+  val elapsedN: string
+  val cpuN: string
+  val gcN: string
+  val timingN: string val timing: Timing.timing -> Markup.T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> Markup.T
   val stateN: string val state: Markup.T
@@ -261,6 +265,20 @@
 val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
 
 
+(* timing *)
+
+val timingN = "timing";
+val elapsedN = "elapsed";
+val cpuN = "cpu";
+val gcN = "gc";
+
+fun timing {elapsed, cpu, gc} =
+  (timingN,
+   [(elapsedN, Time.toString elapsed),
+    (cpuN, Time.toString cpu),
+    (gcN, Time.toString gc)]);
+
+
 (* toplevel *)
 
 val subgoalsN = "subgoals";
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Nov 29 21:50:00 2011 +0100
@@ -168,6 +168,32 @@
   val LOADED_THEORY = "loaded_theory"
 
 
+  /* timing */
+
+  val TIMING = "timing"
+  val ELAPSED = "elapsed"
+  val CPU = "cpu"
+  val GC = "gc"
+
+  object Timing
+  {
+    def apply(timing: isabelle.Timing): Markup =
+      Markup(TIMING, List(
+        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+        (CPU, Properties.Value.Double(timing.cpu.seconds)),
+        (GC, Properties.Value.Double(timing.gc.seconds))))
+    def unapply(markup: Markup): Option[isabelle.Timing] =
+      markup match {
+        case Markup(TIMING, List(
+          (ELAPSED, Properties.Value.Double(elapsed)),
+          (CPU, Properties.Value.Double(cpu)),
+          (GC, Properties.Value.Double(gc)))) =>
+            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+        case _ => None
+      }
+  }
+
+
   /* toplevel */
 
   val SUBGOALS = "subgoals"
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Nov 29 21:50:00 2011 +0100
@@ -15,10 +15,6 @@
   val nameN: string
   val name: string -> T -> T
   val kindN: string
-  val elapsedN: string
-  val cpuN: string
-  val gcN: string
-  val timingN: string val timing: Timing.timing -> T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -67,20 +63,6 @@
 val kindN = "kind";
 
 
-(* timing *)
-
-val timingN = "timing";
-val elapsedN = "elapsed";
-val cpuN = "cpu";
-val gcN = "gc";
-
-fun timing {elapsed, cpu, gc} =
-  (timingN,
-   [(elapsedN, Time.toString elapsed),
-    (cpuN, Time.toString cpu),
-    (gcN, Time.toString gc)]);
-
-
 
 (** print mode operations **)
 
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Nov 29 21:50:00 2011 +0100
@@ -24,32 +24,6 @@
   val Empty = Markup("", Nil)
   val Data = Markup("data", Nil)
   val Broken = Markup("broken", Nil)
-
-
-  /* timing */
-
-  val TIMING = "timing"
-  val ELAPSED = "elapsed"
-  val CPU = "cpu"
-  val GC = "gc"
-
-  object Timing
-  {
-    def apply(timing: isabelle.Timing): Markup =
-      Markup(TIMING, List(
-        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
-        (CPU, Properties.Value.Double(timing.cpu.seconds)),
-        (GC, Properties.Value.Double(timing.gc.seconds))))
-    def unapply(markup: Markup): Option[isabelle.Timing] =
-      markup match {
-        case Markup(TIMING, List(
-          (ELAPSED, Properties.Value.Double(elapsed)),
-          (CPU, Properties.Value.Double(cpu)),
-          (GC, Properties.Value.Double(gc)))) =>
-            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
-        case _ => None
-      }
-  }
 }
 
 
diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/build-jars	Tue Nov 29 21:50:00 2011 +0100
@@ -22,6 +22,7 @@
   General/scan.scala
   General/sha1.scala
   General/symbol.scala
+  General/time.scala
   General/timing.scala
   Isar/keyword.scala
   Isar/outer_syntax.scala