--- 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.
--- 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
--- 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.
--- 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
--- 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}}
--- 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"}
--- 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;
--- 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"}
--- 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
--- 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
--- 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;
--- 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;
--- 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
--- 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;
--- 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;
--- 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;
--- 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));
--- 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 *)
--- 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;
--- 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
--- 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)) =
--- 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);
--- 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";
--- 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"
--- 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] }
}
--- 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 *)
--- 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;
--- 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 =
--- 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);
--- 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)))
}
}
--- 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)) ());
--- 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()
}
}
//}}}
--- 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;
--- 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 () =>
--- 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 ""
--- 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;
--- 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;
--- 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*)
--- 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;
--- 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)));
--- 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 *)
--- 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}
--- 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)));