1.1 --- a/src/Pure/General/timing.ML	Wed Jan 09 14:36:24 2013 +0100
     1.2 +++ b/src/Pure/General/timing.ML	Wed Jan 09 14:59:21 2013 +0100
     1.3 @@ -21,7 +21,6 @@
     1.4    val result: start -> timing
     1.5    val timing: ('a -> 'b) -> 'a -> timing * 'b
     1.6    val is_relevant: timing -> bool
     1.7 -  val properties: timing -> Properties.T
     1.8    val message: timing -> string
     1.9  end
    1.10  
    1.11 @@ -67,17 +66,6 @@
    1.12    in (result start, y) end;
    1.13  
    1.14  
    1.15 -(* properties *)
    1.16 -
    1.17 -fun property name time =
    1.18 -  [(name, Time.toString time)] handle Time.Time => [];
    1.19 -
    1.20 -fun properties {elapsed, cpu, gc} =
    1.21 -  property "time_elapsed" elapsed @
    1.22 -  property "time_cpu" cpu @
    1.23 -  property "time_GC" gc;
    1.24 -
    1.25 -
    1.26  (* timing messages *)
    1.27  
    1.28  val min_time = Time.fromMilliseconds 1;

     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Jan 09 14:36:24 2013 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jan 09 14:59:21 2013 +0100
     2.3 @@ -92,6 +92,7 @@
     2.4    val elapsedN: string
     2.5    val cpuN: string
     2.6    val gcN: string
     2.7 +  val timing_properties: Timing.timing -> Properties.T
     2.8    val timingN: string val timing: Timing.timing -> T
     2.9    val subgoalsN: string
    2.10    val proof_stateN: string val proof_state: int -> T
    2.11 @@ -323,16 +324,17 @@
    2.12  
    2.13  (* timing *)
    2.14  
    2.15 -val timingN = "timing";
    2.16  val elapsedN = "elapsed";
    2.17  val cpuN = "cpu";
    2.18  val gcN = "gc";
    2.19  
    2.20 -fun timing {elapsed, cpu, gc} =
    2.21 -  (timingN,
    2.22 -   [(elapsedN, Time.toString elapsed),
    2.23 -    (cpuN, Time.toString cpu),
    2.24 -    (gcN, Time.toString gc)]);
    2.25 +fun timing_properties {elapsed, cpu, gc} =
    2.26 + [(elapsedN, Time.toString elapsed),
    2.27 +  (cpuN, Time.toString cpu),
    2.28 +  (gcN, Time.toString gc)];
    2.29 +
    2.30 +val timingN = "timing";
    2.31 +fun timing t = (timingN, timing_properties t);
    2.32  
    2.33  
    2.34  (* toplevel *)

     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 09 14:36:24 2013 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 09 14:59:21 2013 +0100
     3.3 @@ -181,25 +181,30 @@
     3.4  
     3.5    /* timing */
     3.6  
     3.7 +  val Elapsed = new Properties.Double("elapsed")
     3.8 +  val CPU = new Properties.Double("cpu")
     3.9 +  val GC = new Properties.Double("gc")
    3.10 +
    3.11 +  object Timing_Properties
    3.12 +  {
    3.13 +    def apply(timing: isabelle.Timing): Properties.T =
    3.14 +      Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
    3.15 +    def unapply(props: Properties.T): Option[isabelle.Timing] =
    3.16 +      (props, props, props) match {
    3.17 +        case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
    3.18 +          Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    3.19 +        case _ => None
    3.20 +      }
    3.21 +  }
    3.22 +
    3.23    val TIMING = "timing"
    3.24 -  val ELAPSED = "elapsed"
    3.25 -  val CPU = "cpu"
    3.26 -  val GC = "gc"
    3.27  
    3.28    object Timing
    3.29    {
    3.30 -    def apply(timing: isabelle.Timing): Markup =
    3.31 -      Markup(TIMING, List(
    3.32 -        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    3.33 -        (CPU, Properties.Value.Double(timing.cpu.seconds)),
    3.34 -        (GC, Properties.Value.Double(timing.gc.seconds))))
    3.35 +    def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
    3.36      def unapply(markup: Markup): Option[isabelle.Timing] =
    3.37        markup match {
    3.38 -        case Markup(TIMING, List(
    3.39 -          (ELAPSED, Properties.Value.Double(elapsed)),
    3.40 -          (CPU, Properties.Value.Double(cpu)),
    3.41 -          (GC, Properties.Value.Double(gc)))) =>
    3.42 -            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    3.43 +        case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
    3.44          case _ => None
    3.45        }
    3.46    }

     4.1 --- a/src/Pure/System/session.ML	Wed Jan 09 14:36:24 2013 +0100
     4.2 +++ b/src/Pure/System/session.ML	Wed Jan 09 14:59:21 2013 +0100
     4.3 @@ -98,7 +98,7 @@
     4.4  
     4.5      val _ =
     4.6        writeln ("\fTiming = " ^ ML_Syntax.print_properties
     4.7 -        ([("threads", threads)] @ Timing.properties timing @ [("factor", factor)]));
     4.8 +        ([("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]));
     4.9      val _ =
    4.10        if verbose then
    4.11          Output.physical_stderr ("Timing " ^ name ^ " (" ^

     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 09 14:36:24 2013 +0100
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 09 14:59:21 2013 +0100
     5.3 @@ -185,6 +185,7 @@
     5.4  ## dependencies
     5.5  
     5.6  if [ -e "$ISABELLE_HOME/Admin/build" ]; then
     5.7 +  "$ISABELLE_TOOL" browser -b || exit $?
     5.8    if [ "$BUILD_JARS" = jars_fresh ]; then
     5.9      "$ISABELLE_TOOL" graphview -b -f || exit $?
    5.10    else