clarified Time vs. Timing;
--- /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"
+}
+
--- 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) =
--- 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
--- 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";
--- 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"
--- 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 **)
--- 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
- }
- }
}
--- 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