clarified Time vs. Timing;
authorwenzelm
Tue Nov 29 21:50:00 2011 +0100 (2011-11-29 ago)
changeset 45674eb65c9d17e2f
parent 45673 cd41e3903fbf
child 45679 a574a9432525
clarified Time vs. Timing;
src/Pure/General/time.scala
src/Pure/General/timing.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/time.scala	Tue Nov 29 21:50:00 2011 +0100
     1.3 @@ -0,0 +1,28 @@
     1.4 +/*  Title:      Pure/General/time.scala
     1.5 +    Module:     PIDE
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Time based on milliseconds.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +object Time
    1.15 +{
    1.16 +  def seconds(s: Double): Time = new Time((s * 1000.0) round)
    1.17 +  def ms(m: Long): Time = new Time(m)
    1.18 +}
    1.19 +
    1.20 +class Time private(val ms: Long)
    1.21 +{
    1.22 +  def seconds: Double = ms / 1000.0
    1.23 +
    1.24 +  def min(t: Time): Time = if (ms < t.ms) this else t
    1.25 +  def max(t: Time): Time = if (ms > t.ms) this else t
    1.26 +
    1.27 +  override def toString =
    1.28 +    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
    1.29 +  def message: String = toString + "s"
    1.30 +}
    1.31 +
     2.1 --- a/src/Pure/General/timing.scala	Tue Nov 29 21:29:53 2011 +0100
     2.2 +++ b/src/Pure/General/timing.scala	Tue Nov 29 21:50:00 2011 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  /*  Title:      Pure/General/timing.scala
     2.5 -    Module:     PIDE
     2.6      Author:     Makarius
     2.7  
     2.8  Basic support for time measurement.
     2.9 @@ -8,25 +7,6 @@
    2.10  package isabelle
    2.11  
    2.12  
    2.13 -object Time
    2.14 -{
    2.15 -  def seconds(s: Double): Time = new Time((s * 1000.0) round)
    2.16 -  def ms(m: Long): Time = new Time(m)
    2.17 -}
    2.18 -
    2.19 -class Time private(val ms: Long)
    2.20 -{
    2.21 -  def seconds: Double = ms / 1000.0
    2.22 -
    2.23 -  def min(t: Time): Time = if (ms < t.ms) this else t
    2.24 -  def max(t: Time): Time = if (ms > t.ms) this else t
    2.25 -
    2.26 -  override def toString =
    2.27 -    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
    2.28 -  def message: String = toString + "s"
    2.29 -}
    2.30 -
    2.31 -
    2.32  object Timing
    2.33  {
    2.34    def timeit[A](message: String)(e: => A) =
     3.1 --- a/src/Pure/PIDE/document.ML	Tue Nov 29 21:29:53 2011 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Tue Nov 29 21:50:00 2011 +0100
     3.3 @@ -308,7 +308,7 @@
     3.4  local
     3.5  
     3.6  fun timing tr t =
     3.7 -  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
     3.8 +  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
     3.9  
    3.10  fun proof_status tr st =
    3.11    (case try Toplevel.proof_of st of
     4.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Tue Nov 29 21:29:53 2011 +0100
     4.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Nov 29 21:50:00 2011 +0100
     4.3 @@ -82,6 +82,10 @@
     4.4    val ignored_spanN: string val ignored_span: Markup.T
     4.5    val malformed_spanN: string val malformed_span: Markup.T
     4.6    val loaded_theoryN: string val loaded_theory: string -> Markup.T
     4.7 +  val elapsedN: string
     4.8 +  val cpuN: string
     4.9 +  val gcN: string
    4.10 +  val timingN: string val timing: Timing.timing -> Markup.T
    4.11    val subgoalsN: string
    4.12    val proof_stateN: string val proof_state: int -> Markup.T
    4.13    val stateN: string val state: Markup.T
    4.14 @@ -261,6 +265,20 @@
    4.15  val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
    4.16  
    4.17  
    4.18 +(* timing *)
    4.19 +
    4.20 +val timingN = "timing";
    4.21 +val elapsedN = "elapsed";
    4.22 +val cpuN = "cpu";
    4.23 +val gcN = "gc";
    4.24 +
    4.25 +fun timing {elapsed, cpu, gc} =
    4.26 +  (timingN,
    4.27 +   [(elapsedN, Time.toString elapsed),
    4.28 +    (cpuN, Time.toString cpu),
    4.29 +    (gcN, Time.toString gc)]);
    4.30 +
    4.31 +
    4.32  (* toplevel *)
    4.33  
    4.34  val subgoalsN = "subgoals";
     5.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Tue Nov 29 21:29:53 2011 +0100
     5.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Nov 29 21:50:00 2011 +0100
     5.3 @@ -168,6 +168,32 @@
     5.4    val LOADED_THEORY = "loaded_theory"
     5.5  
     5.6  
     5.7 +  /* timing */
     5.8 +
     5.9 +  val TIMING = "timing"
    5.10 +  val ELAPSED = "elapsed"
    5.11 +  val CPU = "cpu"
    5.12 +  val GC = "gc"
    5.13 +
    5.14 +  object Timing
    5.15 +  {
    5.16 +    def apply(timing: isabelle.Timing): Markup =
    5.17 +      Markup(TIMING, List(
    5.18 +        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    5.19 +        (CPU, Properties.Value.Double(timing.cpu.seconds)),
    5.20 +        (GC, Properties.Value.Double(timing.gc.seconds))))
    5.21 +    def unapply(markup: Markup): Option[isabelle.Timing] =
    5.22 +      markup match {
    5.23 +        case Markup(TIMING, List(
    5.24 +          (ELAPSED, Properties.Value.Double(elapsed)),
    5.25 +          (CPU, Properties.Value.Double(cpu)),
    5.26 +          (GC, Properties.Value.Double(gc)))) =>
    5.27 +            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    5.28 +        case _ => None
    5.29 +      }
    5.30 +  }
    5.31 +
    5.32 +
    5.33    /* toplevel */
    5.34  
    5.35    val SUBGOALS = "subgoals"
     6.1 --- a/src/Pure/PIDE/markup.ML	Tue Nov 29 21:29:53 2011 +0100
     6.2 +++ b/src/Pure/PIDE/markup.ML	Tue Nov 29 21:50:00 2011 +0100
     6.3 @@ -15,10 +15,6 @@
     6.4    val nameN: string
     6.5    val name: string -> T -> T
     6.6    val kindN: string
     6.7 -  val elapsedN: string
     6.8 -  val cpuN: string
     6.9 -  val gcN: string
    6.10 -  val timingN: string val timing: Timing.timing -> T
    6.11    val no_output: Output.output * Output.output
    6.12    val default_output: T -> Output.output * Output.output
    6.13    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    6.14 @@ -67,20 +63,6 @@
    6.15  val kindN = "kind";
    6.16  
    6.17  
    6.18 -(* timing *)
    6.19 -
    6.20 -val timingN = "timing";
    6.21 -val elapsedN = "elapsed";
    6.22 -val cpuN = "cpu";
    6.23 -val gcN = "gc";
    6.24 -
    6.25 -fun timing {elapsed, cpu, gc} =
    6.26 -  (timingN,
    6.27 -   [(elapsedN, Time.toString elapsed),
    6.28 -    (cpuN, Time.toString cpu),
    6.29 -    (gcN, Time.toString gc)]);
    6.30 -
    6.31 -
    6.32  
    6.33  (** print mode operations **)
    6.34  
     7.1 --- a/src/Pure/PIDE/markup.scala	Tue Nov 29 21:29:53 2011 +0100
     7.2 +++ b/src/Pure/PIDE/markup.scala	Tue Nov 29 21:50:00 2011 +0100
     7.3 @@ -24,32 +24,6 @@
     7.4    val Empty = Markup("", Nil)
     7.5    val Data = Markup("data", Nil)
     7.6    val Broken = Markup("broken", Nil)
     7.7 -
     7.8 -
     7.9 -  /* timing */
    7.10 -
    7.11 -  val TIMING = "timing"
    7.12 -  val ELAPSED = "elapsed"
    7.13 -  val CPU = "cpu"
    7.14 -  val GC = "gc"
    7.15 -
    7.16 -  object Timing
    7.17 -  {
    7.18 -    def apply(timing: isabelle.Timing): Markup =
    7.19 -      Markup(TIMING, List(
    7.20 -        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    7.21 -        (CPU, Properties.Value.Double(timing.cpu.seconds)),
    7.22 -        (GC, Properties.Value.Double(timing.gc.seconds))))
    7.23 -    def unapply(markup: Markup): Option[isabelle.Timing] =
    7.24 -      markup match {
    7.25 -        case Markup(TIMING, List(
    7.26 -          (ELAPSED, Properties.Value.Double(elapsed)),
    7.27 -          (CPU, Properties.Value.Double(cpu)),
    7.28 -          (GC, Properties.Value.Double(gc)))) =>
    7.29 -            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    7.30 -        case _ => None
    7.31 -      }
    7.32 -  }
    7.33  }
    7.34  
    7.35  
     8.1 --- a/src/Pure/build-jars	Tue Nov 29 21:29:53 2011 +0100
     8.2 +++ b/src/Pure/build-jars	Tue Nov 29 21:50:00 2011 +0100
     8.3 @@ -22,6 +22,7 @@
     8.4    General/scan.scala
     8.5    General/sha1.scala
     8.6    General/symbol.scala
     8.7 +  General/time.scala
     8.8    General/timing.scala
     8.9    Isar/keyword.scala
    8.10    Isar/outer_syntax.scala