# HG changeset patch
# User wenzelm
# Date 1365536395 -7200
# Node ID 354c23ef2784371a390a627ab9a425f9f5d6b546
# Parent  5ff01d585a8cf46e6d4edcd7763b67010ef1537c# Parent  b97aeb018900eaab7cb188e66164c3f9ee23b8ac
merged

diff -r 5ff01d585a8c -r 354c23ef2784 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Tue Apr 09 21:39:55 2013 +0200
@@ -85,9 +85,10 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "Toplevel.debug := true"} makes the toplevel print further
-  details about internal error conditions, exceptions being raised
-  etc.
+  \item @{ML "Toplevel.debug := true"} enables low-level exception
+  trace of the ML runtime system.  Note that the result might appear
+  on some raw output window only, outside the formal context of the
+  source text.
 
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
@@ -145,7 +146,6 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
-  @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.theory: "(theory -> theory) ->
@@ -166,10 +166,6 @@
   causes the toplevel loop to echo the result state (in interactive
   mode).
 
-  \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
-  transition should never show timing information, e.g.\ because it is
-  a diagnostic command.
-
   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   function.
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Doc/IsarImplementation/document/root.tex
--- a/src/Doc/IsarImplementation/document/root.tex	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Doc/IsarImplementation/document/root.tex	Tue Apr 09 21:39:55 2013 +0200
@@ -70,6 +70,18 @@
 
   Rob Pike and Brian W. Kernighan
 
+  \vspace*{1cm}
+
+  {\small\em If you look at software today, through the lens of the
+    history of engineering, it's certainly engineering of a sort--but
+    it's the kind of engineering that people without the concept of
+    the arch did. Most software today is very much like an Egyptian
+    pyramid with millions of bricks piled on top of each other, with
+    no structural integrity, but just done by brute force and
+    thousands of slaves.}
+
+  Alan Kay
+
 \end{quote}
 
 \thispagestyle{empty}\clearpage
diff -r 5ff01d585a8c -r 354c23ef2784 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Tue Apr 09 21:39:55 2013 +0200
@@ -362,14 +362,12 @@
   than the fixity declarations of ML and Prolog.
 
   @{rail "
-    @{syntax_def mixfix}: '(' mfix ')'
-    ;
-    @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
-    ;
-
-    mfix: @{syntax template} prios? @{syntax nat}? |
+    @{syntax_def mixfix}: '('
+      @{syntax template} prios? @{syntax nat}? |
       (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
-      @'binder' @{syntax template} prios? @{syntax nat}
+      @'binder' @{syntax template} prios? @{syntax nat} |
+      @'structure'
+    ')'
     ;
     template: string
     ;
@@ -379,13 +377,14 @@
   The string given as @{text template} may include literal text,
   spacing, blocks, and arguments (denoted by ``@{text _}''); the
   special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
-  represents an index argument that specifies an implicit structure
-  reference (see also \secref{sec:locale}).  Infix and binder
-  declarations provide common abbreviations for particular mixfix
-  declarations.  So in practice, mixfix templates mostly degenerate to
-  literal text for concrete syntax, such as ``@{verbatim "++"}'' for
-  an infix symbol.
-*}
+  represents an index argument that specifies an implicit @{keyword
+  "structure"} reference (see also \secref{sec:locale}).  Only locally
+  fixed variables may be declared as @{keyword "structure"}.
+
+  Infix and binder declarations provide common abbreviations for
+  particular mixfix declarations.  So in practice, mixfix templates
+  mostly degenerate to literal text for concrete syntax, such as
+  ``@{verbatim "++"}'' for an infix symbol.  *}
 
 
 subsection {* The general mixfix form *}
@@ -568,9 +567,9 @@
       @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
     (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
-      (@{syntax nameref} @{syntax struct_mixfix} + @'and')
+      (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
-    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and')
+    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
   "}
 
   \begin{description}
@@ -838,7 +837,7 @@
   of @{syntax (inner) logic}.
 
   \item @{syntax_ref (inner) index} denotes an optional index term for
-  indexed syntax.  If omitted, it refers to the first @{keyword
+  indexed syntax.  If omitted, it refers to the first @{keyword_ref
   "structure"} variable in the context.  The special dummy ``@{text
   "\<index>"}'' serves as pattern variable in mixfix annotations that
   introduce indexed notation.
diff -r 5ff01d585a8c -r 354c23ef2784 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy	Tue Apr 09 21:39:55 2013 +0200
@@ -514,8 +514,8 @@
   \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
   parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
   are optional).  The special syntax declaration ``@{text
-  "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
-  implicitly in this context.
+  "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may
+  be referenced implicitly in this context.
 
   \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
   constraint @{text \<tau>} on the local parameter @{text x}.  This
diff -r 5ff01d585a8c -r 354c23ef2784 src/Doc/isar.sty
--- a/src/Doc/isar.sty	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Doc/isar.sty	Tue Apr 09 21:39:55 2013 +0200
@@ -17,7 +17,6 @@
 \newcommand{\isasymBEGIN}{\isakeyword{begin}}
 \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
 \newcommand{\isasymIN}{\isakeyword{in}}
-\newcommand{\isasymSTRUCTURE}{\isakeyword{structure}}
 \newcommand{\isasymFIXES}{\isakeyword{fixes}}
 \newcommand{\isasymASSUMES}{\isakeyword{assumes}}
 \newcommand{\isasymSHOWS}{\isakeyword{shows}}
diff -r 5ff01d585a8c -r 354c23ef2784 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -329,8 +329,7 @@
    Scan.succeed (boogie_status_vc false)) --
   vc_name >> (fn (f, vc_name) => f vc_name)
 
-fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
-  f (Toplevel.theory_of state))
+fun status_cmd f = Toplevel.keep (f o Toplevel.theory_of)
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "boogie_status"}
diff -r 5ff01d585a8c -r 354c23ef2784 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/HOL/Orderings.thy	Tue Apr 09 21:39:55 2013 +0200
@@ -492,8 +492,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_orders"}
     "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-        Toplevel.keep (print_structures o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (print_structures o Toplevel.context_of)));
 
 end;
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -81,10 +81,8 @@
 fun string_of_status NONE = "(unproved)"
   | string_of_status (SOME _) = "(proved)";
 
-fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state =>
+fun show_status thy (p, f) =
   let
-    val thy = Toplevel.theory_of state;
-
     val (context, defs, vcs) = SPARK_VCs.get_vcs thy true;
 
     val vcs' = AList.coalesce (op =) (map_filter
@@ -93,8 +91,7 @@
            SOME (trace, (name, status, ctxt, stmt))
          else NONE) vcs);
 
-    val ctxt = state |>
-      Toplevel.theory_of |>
+    val ctxt = thy |>
       Proof_Context.init_global |>
       Context.proof_map (fold Element.init context)
   in
@@ -116,7 +113,7 @@
            (Element.pretty_ctxt ctxt context' @
             Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
     Pretty.chunks2 |> Pretty.writeln
-  end);
+  end;
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_open"}
@@ -165,7 +162,8 @@
        (Args.parens
           (   Args.$$$ "proved" >> K (is_some, K "")
            || Args.$$$ "unproved" >> K (is_none, K "")))
-       (K true, string_of_status) >> show_status);
+       (K true, string_of_status) >> (fn args =>
+        Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_end"}
diff -r 5ff01d585a8c -r 354c23ef2784 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -123,9 +123,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
     "find theorems with (potentially) superfluous assumptions"
-    (Scan.option Parse.name
-      >> (fn opt_thy_name =>
-        Toplevel.no_timing o Toplevel.keep (fn state =>
-          print_unused_assms (Toplevel.context_of state) opt_thy_name)))
+    (Scan.option Parse.name >> (fn name =>
+      Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
 
 end
diff -r 5ff01d585a8c -r 354c23ef2784 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -249,7 +249,6 @@
   Outer_Syntax.improper_command @{command_spec "smt_status"}
     "show the available SMT solvers, the currently selected SMT solver, \
     \and the values of SMT configuration options"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
-      print_setup (Toplevel.context_of state))))
+    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
 end
diff -r 5ff01d585a8c -r 354c23ef2784 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -1175,8 +1175,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_inductives"}
     "print (co)inductive definitions and monotonicity rules"
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_context o
-        Toplevel.keep (print_inductives o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.unknown_context o
+      Toplevel.keep (print_inductives o Toplevel.context_of)));
 
 end;
diff -r 5ff01d585a8c -r 354c23ef2784 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Provers/classical.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -968,9 +968,6 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (fn state =>
-        let val ctxt = Toplevel.context_of state
-        in print_claset ctxt end)));
+    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
 
 end;
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -203,10 +203,7 @@
         ("workers_active", Markup.print_int active),
         ("workers_waiting", Markup.print_int waiting)] @
         ML_Statistics.get ();
-    in
-      Output.protocol_message (Markup.ML_statistics :: stats) ""
-        handle Fail msg => warning msg
-    end
+    in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
   else ();
 
 
@@ -253,8 +250,7 @@
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     val _ =
       if ! Multithreading.trace >= 2 then
-        Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
-          handle Fail msg => warning msg
+        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
       else ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/General/output.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -24,6 +24,7 @@
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
+  exception Protocol_Message of Properties.T
   structure Private_Hooks:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
@@ -45,6 +46,7 @@
   val report: string -> unit
   val result: serial * string -> unit
   val protocol_message: Properties.T -> string -> unit
+  val try_protocol_message: Properties.T -> string -> unit
 end;
 
 structure Output: OUTPUT =
@@ -88,6 +90,8 @@
 
 (* Isabelle output channels *)
 
+exception Protocol_Message of Properties.T;
+
 structure Private_Hooks =
 struct
   val writeln_fn = Unsynchronized.ref physical_writeln;
@@ -100,7 +104,7 @@
   val report_fn = Unsynchronized.ref (fn _: output => ());
   val result_fn = Unsynchronized.ref (fn _: serial * output => ());
   val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
-    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
+    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
@@ -114,6 +118,7 @@
 fun report s = ! Private_Hooks.report_fn (output s);
 fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
 fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
+fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
 
 end;
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/General/properties.ML	Tue Apr 09 21:39:55 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 5ff01d585a8c -r 354c23ef2784 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/General/timing.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -23,7 +23,8 @@
   val is_relevant_time: Time.time -> bool
   val is_relevant: timing -> bool
   val message: timing -> string
-  val status: ('a -> 'b) -> 'a -> 'b
+  val protocol_message: Properties.T -> timing -> unit
+  val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b
 end
 
 structure Timing: TIMING =
@@ -103,10 +104,13 @@
 fun timeap f x = timeit (fn () => f x);
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
-fun status f x =
+fun protocol_message props t =
+  Output.try_protocol_message (props @ Markup.timing_properties t) "";
+
+fun protocol props f x =
   let
     val (t, result) = timing (Exn.interruptible_capture f) x;
-    val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else ();
+    val _ = protocol_message props t;
   in Exn.release result end;
 
 end;
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -208,13 +208,13 @@
 val _ =
   Outer_Syntax.local_theory @{command_spec "notation"}
     "add concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "no_notation"}
     "delete concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 
@@ -281,7 +281,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
-    (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
+    (Parse.ML_source >> Isar_Cmd.ml_diag false);
 
 val _ =
   Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
@@ -381,7 +381,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_bundles"}
     "print bundles of declarations"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
 
 
@@ -604,7 +604,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
-    (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
+    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
 val case_spec =
@@ -746,197 +746,193 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
     "change default margin for pretty printing"
-    (Parse.nat >>
-      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
+    (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "help"}
     "retrieve outer syntax commands according to name patterns"
-    (Scan.repeat Parse.name >> (fn pats =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
+    (Scan.repeat Parse.name >>
+      (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
+    (Scan.succeed (Toplevel.imperative Outer_Syntax.print_outer_syntax));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Attrib.print_configs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep Toplevel.print_state_context));
+    (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theory"}
     "print logical theory contents (verbose!)"
-    (opt_bang >> (fn b => Toplevel.no_timing o Toplevel.unknown_theory o
+    (opt_bang >> (fn b => Toplevel.unknown_theory o
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_syntax"}
     "print inner syntax of context (verbose!)"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
     "print definitional rewrite rules of context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
     "print constant abbreviations of context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theorems"}
     "print theorems of local theory or proof context"
-    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
+    (opt_bang >> Isar_Cmd.print_theorems);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locales"}
     "print locales of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_classes"}
     "print classes of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_locale"}
     "print locale of this theory"
     (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
-      Toplevel.no_timing o Toplevel.unknown_theory o
+      Toplevel.unknown_theory o
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_interps"}
     "print interpretations of locale for this theory or proof context"
-    (Parse.position Parse.xname >> (fn name => Toplevel.no_timing o Toplevel.unknown_context o
+    (Parse.position Parse.xname >> (fn name =>
+      Toplevel.unknown_context o
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_dependencies"}
     "print dependencies of locale expression"
-    (opt_bang -- Parse_Spec.locale_expression true >> (fn (clean, expr) =>
-      Toplevel.no_timing o Toplevel.unknown_context o
-        Toplevel.keep (fn state =>
-          Expression.print_dependencies (Toplevel.context_of state) clean expr)));
+    (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
+      Toplevel.unknown_context o
+      Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_attributes"}
     "print attributes of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_simpset"}
     "print context of Simplifier"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (fn state =>
         let val ctxt = Toplevel.context_of state
         in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+    (Scan.succeed (Toplevel.unknown_theory o
       Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
+    (Scan.succeed Isar_Cmd.thy_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.locale_deps));
+    (Scan.succeed Isar_Cmd.locale_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
+    (Scan.succeed Isar_Cmd.class_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
-    (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
+    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_statement"}
     "print theorems as long statements"
-    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
+    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_stmts);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
-    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
+    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_thms);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
-    (opt_modes -- Scan.option Parse_Spec.xthms1
-      >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
+    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
-    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
+    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
-    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
+    (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
-    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
+    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
     (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
-      >> (Toplevel.no_timing oo Isar_Cmd.print_type));
+      >> Isar_Cmd.print_type);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
-        (Code.print_codesetup o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.unknown_theory o
+      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
     (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
-       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
-         (Toplevel.no_timing oo Isar_Cmd.unused_thms));
+       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
 
 
 
@@ -944,44 +940,40 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
-    (Parse.path >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => File.cd (Path.explode name))));
+    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
-    (Scan.succeed (Toplevel.no_timing o
-      Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
+    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
-    (Parse.position Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
+    (Parse.position Parse.name >>
+      (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
-    (Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
+    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "kill_thy"}
     "kill theory -- try to remove from loader database"
-    (Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
+    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "display_drafts"}
     "display raw source files with symbols"
-    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
+    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_drafts"}
     "print raw source files with symbols"
-    (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
+    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
 
 val _ =  (* FIXME tty only *)
   Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
-      Toplevel.no_timing o Toplevel.keep (fn state =>
+      Toplevel.keep (fn state =>
        (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
@@ -989,32 +981,32 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "disable_pr"}
     "disable printing of toplevel state"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
+    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "enable_pr"}
     "enable printing of toplevel state"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
+    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "commit"}
     "commit current session to ML session image"
-    (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
+    (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle"
-    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
+    (Parse.opt_unit >> (K (Toplevel.imperative quit)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
     (Scan.succeed
-      (Toplevel.no_timing o Toplevel.keep (fn state =>
+      (Toplevel.keep (fn state =>
         (Context.set_thread_data (try Toplevel.generic_theory_of state);
           raise Runtime.TERMINATE))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o Session.welcome)));
+    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
 
 
 
@@ -1022,22 +1014,22 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
+    (Scan.succeed (Toplevel.imperative Isar.init));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
     (Scan.optional Parse.nat 1 >>
-      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
+      (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
     (Scan.optional Parse.nat 1 >>
-      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
+      (fn n => Toplevel.imperative (fn () => Isar.undo n)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "undos_proof"}
     "undo commands (skipping closed proofs)"
-    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
+    (Scan.optional Parse.nat 1 >> (fn n =>
       Toplevel.keep (fn state =>
         if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
 
@@ -1045,13 +1037,13 @@
   Outer_Syntax.improper_command @{command_spec "cannot_undo"}
     "partial undo -- Proof General legacy"
     (Parse.name >>
-      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
+      (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "kill"}
     "kill partial proof or theory development"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
+    (Scan.succeed (Toplevel.imperative Isar.kill));
 
 
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -298,6 +298,8 @@
 
 (* mixfix annotations *)
 
+local
+
 val mfix = string --
   !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
     Scan.optional nat 1000) >> (Mixfix o triple2);
@@ -305,18 +307,25 @@
 val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
 val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
 val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
+val strcture = $$$ "structure" >> K Structure;
 
 val binder = $$$ "binder" |--
   !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
   >> (Binder o triple2);
 
-fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
-fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
+val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
+
+fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")");
+fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
+
+in
 
-val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
-val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
-val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
-val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
+val mixfix = annotation !!! mixfix_body;
+val mixfix' = annotation I mixfix_body;
+val opt_mixfix = opt_annotation !!! mixfix_body;
+val opt_mixfix' = opt_annotation I mixfix_body;
+
+end;
 
 
 (* fixes *)
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -20,7 +20,6 @@
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   val includes: (xstring * Position.T) list parser
-  val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expression: string list parser
@@ -83,12 +82,8 @@
 
 val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
 
-val locale_mixfix =
-  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
-  Parse.mixfix;
-
 val locale_fixes =
-  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
+  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
     >> (single o Parse.triple1) ||
   Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -1154,16 +1154,20 @@
 end;
 
 
-(* terminal proofs *)
+(* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
 
 local
 
 fun future_terminal_proof proof1 proof2 done int state =
   if Goal.future_enabled_level 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
-      Goal.fork_params
-        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
-        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
+      let
+        val pos = Position.thread_data ();
+        val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
+      in
+        Goal.fork_params {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
+          (fn () => ((), Timing.protocol props proof2 state'))
+      end) |> snd |> done
   else proof1 state;
 
 in
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -76,7 +76,9 @@
         (case msgs of
           [] => "exception " ^ name ^ " raised" ^ pos
         | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
-        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
+        | _ =>
+            cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") ::
+              map (Markup.markup Markup.item) msgs))
       end;
 
     fun exn_msgs (context, ((i, exn), id)) =
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -42,7 +42,6 @@
   val interactive: bool -> transition -> transition
   val set_print: bool -> transition -> transition
   val print: transition -> transition
-  val no_timing: transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
@@ -90,7 +89,6 @@
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
-  val approximative_id: transition -> {file: string, offset: int, name: string} option
   val get_timing: transition -> Time.time option
   val put_timing: Time.time option -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
@@ -346,18 +344,17 @@
   pos: Position.T,           (*source position*)
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
-  no_timing: bool,           (*suppress timing*)
   timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
+fun make_transition (name, pos, int_only, print, timing, trans) =
   Transition {name = name, pos = pos, int_only = int_only, print = print,
-    no_timing = no_timing, timing = timing, trans = trans};
+    timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
-  make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
+fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
+  make_transition (f (name, pos, int_only, print, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, false, NONE, []);
+val empty = make_transition ("", Position.none, false, false, NONE, []);
 
 
 (* diagnostics *)
@@ -375,26 +372,23 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
-fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
-fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
-val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
-  (name, pos, int_only, print, true, timing, trans));
-
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
+  (name, pos, int_only, print, timing, tr :: trans));
 
-val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
-  (name, pos, int_only, print, no_timing, timing, []));
+val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
+  (name, pos, int_only, print, timing, []));
 
-fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
 val print = set_print true;
 
@@ -596,19 +590,6 @@
 fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
 
 
-(* approximative identification within source file *)
-
-fun approximative_id tr =
-  let
-    val name = name_of tr;
-    val pos = pos_of tr;
-  in
-    (case (Position.file_of pos, Position.offset_of pos) of
-      (SOME file, SOME offset) => SOME {file = file, offset = offset, name = name}
-    | _ => NONE)
-  end;
-
-
 (* thread position *)
 
 fun setmp_thread_position (Transition {pos, ...}) f x =
@@ -633,41 +614,24 @@
 (* apply transitions *)
 
 fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
-  (name, pos, int_only, print, no_timing, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
+  (name, pos, int_only, print, timing, trans));
 
 local
 
-fun app int (tr as Transition {trans, print, no_timing, ...}) =
+fun app int (tr as Transition {trans, print, ...}) =
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
 
       val (result, opt_err) =
-         state |>
-          (apply_trans int trans
-            |> (! profiling > 0 andalso not no_timing) ? profile (! profiling));
+         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
       val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
 
       val timing_result = Timing.result timing_start;
-
-      val _ =
-        if Timing.is_relevant timing_result andalso
-          (! profiling > 0 orelse ! timing andalso not no_timing)
-        then warning (command_msg "" tr ^ ": " ^ Timing.message timing_result)
-        else ();
-      val _ =
-        if Timing.is_relevant timing_result
-        then status tr (Markup.timing timing_result)
-        else ();
-      val _ =
-        (case approximative_id tr of
-          SOME id =>
-            (Output.protocol_message
-              (Markup.command_timing ::
-                Markup.command_timing_properties id (#elapsed timing_result)) ""
-            handle Fail _ => ())
-        | NONE => ());
+      val timing_props =
+        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
+      val _ = Timing.protocol_message timing_props timing_result;
     in
       (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
     end);
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Apr 09 21:39:55 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";
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Apr 09 21:39:55 2013 +0200
@@ -193,6 +193,7 @@
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
+
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
@@ -206,6 +207,7 @@
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
+
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
@@ -214,6 +216,22 @@
   }
 
 
+  /* command timing */
+
+  object Command_Timing
+  {
+    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+      props match {
+        case (FUNCTION, "command_timing") :: args =>
+          (args, args) match {
+            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
+
   /* toplevel */
 
   val SUBGOALS = "subgoals"
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/PIDE/xml.scala	Tue Apr 09 21:39:55 2013 +0200
@@ -145,53 +145,54 @@
 
     private def trim_bytes(s: String): String = new String(s.toCharArray)
 
-    private def _cache_string(x: String): String =
+    private def cache_string(x: String): String =
       lookup(x) match {
         case Some(y) => y
         case None =>
           val z = trim_bytes(x)
           if (z.length > max_string) z else store(z)
       }
-    private def _cache_props(x: Properties.T): Properties.T =
+    private def cache_props(x: Properties.T): Properties.T =
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
-          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
+          case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
         }
-    private def _cache_markup(x: Markup): Markup =
+    private def cache_markup(x: Markup): Markup =
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case Markup(name, props) =>
-              store(Markup(_cache_string(name), _cache_props(props)))
+              store(Markup(cache_string(name), cache_props(props)))
           }
       }
-    private def _cache_tree(x: XML.Tree): XML.Tree =
+    private def cache_tree(x: XML.Tree): XML.Tree =
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case XML.Elem(markup, body) =>
-              store(XML.Elem(_cache_markup(markup), _cache_body(body)))
-            case XML.Text(text) => store(XML.Text(_cache_string(text)))
+              store(XML.Elem(cache_markup(markup), cache_body(body)))
+            case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
-    private def _cache_body(x: XML.Body): XML.Body =
+    private def cache_body(x: XML.Body): XML.Body =
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
-          case None => x.map(_cache_tree(_))
+          case None => x.map(cache_tree(_))
         }
 
     // main methods
-    def cache_string(x: String): String = synchronized { _cache_string(x) }
-    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
-    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
-    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
-    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
+    def string(x: String): String = synchronized { cache_string(x) }
+    def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
+    def markup(x: Markup): Markup = synchronized { cache_markup(x) }
+    def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
+    def body(x: XML.Body): XML.Body = synchronized { cache_body(x) }
+    def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
   }
 
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -193,37 +193,34 @@
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+    (Scan.succeed (Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
 val _ = (*undo without output -- historical*)
   Outer_Syntax.improper_command
     (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
+    (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)"
-    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
+    (Parse.opt_unit >> (K (Toplevel.imperative restart)));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)"
-    (Scan.succeed (Toplevel.no_timing o
-      Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
+    (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)"
-    (Parse.name >> (fn file =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
+    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file)));
 
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)"
-    (Parse.name >> (Toplevel.no_timing oo
-      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
+    (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
 
 
 (* init *)
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -1031,10 +1031,10 @@
 val _ =
   Outer_Syntax.improper_command
     (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
-    (Parse.text >> (Toplevel.no_timing oo
+    (Parse.text >>
       (fn txt => Toplevel.imperative (fn () =>
         if print_mode_active proof_general_emacsN
         then process_pgip_emacs txt
-        else process_pgip_plain txt))));
+        else process_pgip_plain txt)));
 
 end;
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Syntax/local_syntax.ML
     Author:     Makarius
 
-Local syntax depending on theory syntax.
+Local syntax depending on theory syntax, with special support for
+implicit structure references.
 *)
 
 signature LOCAL_SYNTAX =
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -250,7 +250,8 @@
 fun the_struct [] = error "Illegal reference to implicit structure"
   | the_struct (x :: _) = x;
 
-fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs)
+fun struct_tr structs [Const ("_indexdefault", _)] =
+      Syntax.const (Lexicon.mark_fixed (the_struct structs))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Apr 09 21:39:55 2013 +0200
@@ -82,13 +82,13 @@
 
   /* output */
 
+  val xml_cache = new XML.Cache()
+
   private def system_output(text: String)
   {
     receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
-  private val xml_cache = new XML.Cache()
-
   private def output_message(kind: String, props: Properties.T, body: XML.Body)
   {
     if (kind == Markup.INIT) system_channel.accepted()
@@ -97,8 +97,7 @@
     else {
       val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
       val reports = Protocol.message_reports(props, body)
-      for (msg <- main :: reports)
-        receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
+      for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg)))
     }
   }
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/System/isar.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -118,6 +118,23 @@
 
 local
 
+fun protocol_message props output =
+  (case props of
+    function :: args =>
+      if function = Markup.command_timing then
+        let
+          val name = the_default "" (Properties.get args Markup.nameN);
+          val pos = Position.of_properties args;
+          val timing = Markup.parse_timing_properties args;
+        in
+          if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
+            andalso name <> "" andalso not (Keyword.is_control name)
+          then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
+          else ()
+        end
+      else raise Output.Protocol_Message props
+  | [] => raise Output.Protocol_Message props);
+
 fun raw_loop secure src =
   let
     fun check_secure () =
@@ -139,6 +156,7 @@
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
   if do_init then (Options.load_default (); init ()) else ();
+  Output.Private_Hooks.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/System/session.scala	Tue Apr 09 21:39:55 2013 +0200
@@ -300,22 +300,31 @@
     def handle_output(output: Isabelle_Process.Output)
     //{{{
     {
-      def bad_output(output: Isabelle_Process.Output)
+      def bad_output()
       {
         if (verbose)
           System.err.println("Ignoring prover output: " + output.message.toString)
       }
 
+      def accumulate(state_id: Document.ID, message: XML.Elem)
+      {
+        try {
+          val st = global_state >>> (_.accumulate(state_id, message))
+          delay_commands_changed.invoke(false, List(st.command))
+        }
+        catch {
+          case _: Document.State.Fail => bad_output()
+        }
+      }
+
       output.properties match {
 
         case Position.Id(state_id) if !output.is_protocol =>
-          try {
-            val st = global_state >>> (_.accumulate(state_id, output.message))
-            delay_commands_changed.invoke(false, List(st.command))
-          }
-          catch {
-            case _: Document.State.Fail => bad_output(output)
-          }
+          accumulate(state_id, output.message)
+
+        case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
+          val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
+          accumulate(state_id, prover.get.xml_cache.elem(message))
 
         case Markup.Assign_Execs if output.is_protocol =>
           XML.content(output.body) match {
@@ -324,8 +333,8 @@
                 val cmds = global_state >>> (_.assign(id, assign))
                 delay_commands_changed.invoke(true, cmds)
               }
-              catch { case _: Document.State.Fail => bad_output(output) }
-            case _ => bad_output(output)
+              catch { case _: Document.State.Fail => bad_output() }
+            case _ => bad_output()
           }
           // FIXME separate timeout event/message!?
           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
@@ -340,8 +349,8 @@
               try {
                 global_state >> (_.removed_versions(removed))
               }
-              catch { case _: Document.State.Fail => bad_output(output) }
-            case _ => bad_output(output)
+              catch { case _: Document.State.Fail => bad_output() }
+            case _ => bad_output()
           }
 
         case Markup.Invoke_Scala(name, id) if output.is_protocol =>
@@ -374,7 +383,7 @@
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
 
-        case _ => bad_output(output)
+        case _ => bad_output()
       }
     }
     //}}}
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -265,7 +265,7 @@
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => ();
+    val _ = Output.try_protocol_message (Markup.loading_theory name) "";
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Tools/build.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -12,29 +12,62 @@
 structure Build: BUILD =
 struct
 
+(* command timings *)
+
+type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
+
+val empty_timings: timings = Symtab.empty;
+
+fun update_timings props =
+  (case Markup.parse_command_timing_properties props of
+    SOME ({file, offset, name}, time) =>
+      Symtab.map_default (file, Inttab.empty)
+        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
+  | NONE => I);
+
+fun approximative_id name pos =
+  (case (Position.file_of pos, Position.offset_of pos) of
+    (SOME file, SOME offset) =>
+      if name = "" then NONE else SOME {file = file, offset = offset, name = name}
+  | _ => NONE);
+
+fun lookup_timings timings tr =
+  (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
+    SOME {file, offset, name} =>
+      (case Symtab.lookup timings file of
+        SOME offsets =>
+          (case Inttab.lookup offsets offset of
+            SOME (name', time) => if name = name' then SOME time else NONE
+          | NONE => NONE)
+      | NONE => NONE)
+  | NONE => NONE);
+
+
 (* protocol messages *)
 
-local
-
-(* FIXME avoid hardwired stuff!? *)
-val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
-
-fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
-
-in
+fun inline_message a args =
+  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
 
 fun protocol_message props output =
   (case props of
     function :: args =>
-      if member (op =) protocol_echo function then
-        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
+      if function = Markup.ML_statistics orelse function = Markup.task_statistics then
+        inline_message (#2 function) args
+      else if function = Markup.command_timing then
+        let
+          val name = the_default "" (Properties.get args Markup.nameN);
+          val pos = Position.of_properties args;
+          val {elapsed, ...} = Markup.parse_timing_properties args;
+        in
+          (case approximative_id name pos of
+            SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
+          | NONE => ())
+        end
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
-        | NONE => protocol_undef ())
-  | [] => protocol_undef ());
-
-end;
+        | NONE => raise Output.Protocol_Message props)
+  | [] => raise Output.Protocol_Message props);
 
 
 (* build *)
@@ -82,30 +115,6 @@
           " (undefined " ^ commas conds ^ ")\n"))
   end;
 
-
-(* command timings *)
-
-type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
-
-val empty_timings: timings = Symtab.empty;
-
-fun update_timings props =
-  (case Markup.parse_command_timing_properties props of
-    SOME ({file, offset, name}, time) =>
-      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
-  | NONE => I);
-
-fun lookup_timings timings tr =
-  (case Toplevel.approximative_id tr of
-    SOME {file, offset, name} =>
-      (case Symtab.lookup timings file of
-        SOME offsets =>
-          (case Inttab.lookup offsets offset of
-            SOME (name', time) => if name = name' then SOME time else NONE
-          | NONE => NONE)
-      | NONE => NONE)
-  | NONE => NONE);
-
 in
 
 fun build args_file = Command_Line.tool (fn () =>
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 09 21:39:55 2013 +0200
@@ -595,7 +595,7 @@
     val lines = split_lines(text)
     val xml_cache = new XML.Cache()
     def parse_lines(prfx: String): List[Properties.T] =
-      Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
+      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
 
     val name =
       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Tools/find_consts.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -139,8 +139,7 @@
   Outer_Syntax.improper_command @{command_spec "find_consts"}
     "find constants by name/type patterns"
     (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
-      >> (fn spec => Toplevel.no_timing o
-        Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
+      >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
 
 end;
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -628,7 +628,6 @@
     "find theorems meeting specified criteria"
     (options -- query_parser
       >> (fn ((opt_lim, rem_dups), spec) =>
-        Toplevel.no_timing o
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;
diff -r 5ff01d585a8c -r 354c23ef2784 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -505,8 +505,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
-    (Scan.succeed
-      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
-        (print_codeproc o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.unknown_theory o
+      Toplevel.keep (print_codeproc o Toplevel.theory_of)));
 
 end; (*struct*)
diff -r 5ff01d585a8c -r 354c23ef2784 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -1058,16 +1058,16 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_thms"}
     "print system of code equations for code"
-    (Scan.repeat1 Parse.term_group
-      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+    (Scan.repeat1 Parse.term_group >> (fn cs =>
+      Toplevel.unknown_theory o
+      Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_deps"}
     "visualize dependencies of code equations for code"
-    (Scan.repeat1 Parse.term_group
-      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+    (Scan.repeat1 Parse.term_group >> (fn cs =>
+      Toplevel.unknown_theory o
+      Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));
 
 end;
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Tools/induct.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -261,7 +261,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
     "print induction and cases rules"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
diff -r 5ff01d585a8c -r 354c23ef2784 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Tools/quickcheck.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -533,7 +533,7 @@
   Outer_Syntax.improper_command @{command_spec "quickcheck"}
     "try to find counterexample for subgoal"
     (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
-      Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
+      Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
 
 
 (* automatic testing *)
diff -r 5ff01d585a8c -r 354c23ef2784 src/Tools/value.ML
--- a/src/Tools/value.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/Tools/value.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -65,8 +65,7 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
     (opt_evaluator -- opt_modes -- Parse.term
-      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
-          (value_cmd some_name modes t)));
+      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
 val antiq_setup =
   Thy_Output.antiquotation @{binding value}
diff -r 5ff01d585a8c -r 354c23ef2784 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue Apr 09 16:32:04 2013 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Apr 09 21:39:55 2013 +0200
@@ -122,7 +122,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));