--- a/src/HOL/Decision_Procs/approximation.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML Mon Nov 03 14:50:27 2014 +0100
@@ -151,7 +151,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val _ =
- Outer_Syntax.improper_command @{command_spec "approximate"} "print approximation of term"
+ Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
(opt_modes -- Parse.term
>> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML Mon Nov 03 14:50:27 2014 +0100
@@ -246,7 +246,7 @@
end
val _ =
- Outer_Syntax.improper_command @{command_spec "old_smt_status"}
+ Outer_Syntax.command @{command_spec "old_smt_status"}
"show the available SMT solvers, the currently selected SMT solver, \
\and the values of SMT configuration options"
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
--- a/src/HOL/Library/refute.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Library/refute.ML Mon Nov 03 14:50:27 2014 +0100
@@ -2967,7 +2967,7 @@
(* 'refute' command *)
val _ =
- Outer_Syntax.improper_command @{command_spec "refute"}
+ Outer_Syntax.command @{command_spec "refute"}
"try to find a model that refutes a given subgoal"
(scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
--- a/src/HOL/Orderings.thy Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Orderings.thy Mon Nov 03 14:50:27 2014 +0100
@@ -439,7 +439,7 @@
end;
val _ =
- Outer_Syntax.improper_command @{command_spec "print_orders"}
+ Outer_Syntax.command @{command_spec "print_orders"}
"print order structures available to transitivity reasoner"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_structures o Toplevel.context_of)));
--- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Nov 03 14:50:27 2014 +0100
@@ -126,7 +126,7 @@
(Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
val _ =
- Outer_Syntax.improper_command @{command_spec "spark_status"}
+ Outer_Syntax.command @{command_spec "spark_status"}
"show the name and state of all loaded verification conditions"
(Scan.optional
(Args.parens
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Nov 03 14:50:27 2014 +0100
@@ -912,7 +912,7 @@
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
- Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
+ Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
(Parse.path >> (fn name =>
Toplevel.theory (fn thy =>
let val path = Path.explode name
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Nov 03 14:50:27 2014 +0100
@@ -1866,7 +1866,7 @@
(*This has been disabled since it requires a hook to be specified to use "import_thm"
val _ =
- Outer_Syntax.improper_command @{command_spec "import_leo2_proof"} "import TPTP proof"
+ Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
(Parse.path >> (fn name =>
Toplevel.theory (fn thy =>
let val path = Path.explode name
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Nov 03 14:50:27 2014 +0100
@@ -1598,7 +1598,7 @@
end;
val _ =
- Outer_Syntax.improper_command @{command_spec "print_bnfs"}
+ Outer_Syntax.command @{command_spec "print_bnfs"}
"print all bounded natural functors"
(Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Nov 03 14:50:27 2014 +0100
@@ -630,7 +630,7 @@
end;
val _ =
- Outer_Syntax.improper_command @{command_spec "print_case_translations"}
+ Outer_Syntax.command @{command_spec "print_case_translations"}
"print registered case combinators and constructors"
(Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Nov 03 14:50:27 2014 +0100
@@ -532,11 +532,11 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
+ Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
+ Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
end
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Nov 03 14:50:27 2014 +0100
@@ -374,7 +374,7 @@
|> sort_strings |> cat_lines)))))
val _ =
- Outer_Syntax.improper_command @{command_spec "nitpick"}
+ Outer_Syntax.command @{command_spec "nitpick"}
"try to find a counterexample for a given subgoal using Nitpick"
(parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
Toplevel.unknown_proof o
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Nov 03 14:50:27 2014 +0100
@@ -1028,7 +1028,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
val _ =
- Outer_Syntax.improper_command @{command_spec "values_prolog"}
+ Outer_Syntax.command @{command_spec "values_prolog"}
"enumerate and print comprehensions"
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
>> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t)))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Nov 03 14:50:27 2014 +0100
@@ -287,7 +287,7 @@
(opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
val _ =
- Outer_Syntax.improper_command @{command_spec "values"}
+ Outer_Syntax.command @{command_spec "values"}
"enumerate and print comprehensions"
(opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
>> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Nov 03 14:50:27 2014 +0100
@@ -111,7 +111,7 @@
end
val _ =
- Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
+ Outer_Syntax.command @{command_spec "find_unused_assms"}
"find theorems with (potentially) superfluous assumptions"
(Scan.option Parse.name >> (fn name =>
Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon Nov 03 14:50:27 2014 +0100
@@ -229,15 +229,15 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
+ Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
+ Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
+ Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
end;
--- a/src/HOL/Tools/SMT/smt_config.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Nov 03 14:50:27 2014 +0100
@@ -241,7 +241,7 @@
end
val _ =
- Outer_Syntax.improper_command @{command_spec "smt_status"}
+ Outer_Syntax.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.keep (print_setup o Toplevel.context_of)))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Nov 03 14:50:27 2014 +0100
@@ -386,7 +386,7 @@
no_fact_override
val _ =
- Outer_Syntax.improper_command @{command_spec "sledgehammer"}
+ Outer_Syntax.command @{command_spec "sledgehammer"}
"search for first-order proof using automatic theorem provers"
((Scan.optional Parse.name runN -- parse_params
-- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
--- a/src/HOL/Tools/inductive.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Mon Nov 03 14:50:27 2014 +0100
@@ -1179,7 +1179,7 @@
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_inductives"}
+ Outer_Syntax.command @{command_spec "print_inductives"}
"print (co)inductive definitions and monotonicity rules"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_inductives o Toplevel.context_of)));
--- a/src/HOL/Tools/try0.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/try0.ML Mon Nov 03 14:50:27 2014 +0100
@@ -180,7 +180,7 @@
|| Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
val _ =
- Outer_Syntax.improper_command @{command_spec "try0"} "try a combination of proof methods"
+ Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
(Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
--- a/src/HOL/Tools/value.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/value.ML Mon Nov 03 14:50:27 2014 +0100
@@ -70,7 +70,7 @@
Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
val _ =
- Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
+ Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Nov 03 14:50:27 2014 +0100
@@ -36,7 +36,7 @@
subsection {* Outer syntax: cartouche within command syntax *}
ML {*
- Outer_Syntax.improper_command @{command_spec "cartouche"} ""
+ Outer_Syntax.command @{command_spec "cartouche"} ""
(Parse.cartouche >> (fn s =>
Toplevel.imperative (fn () => writeln s)))
*}
@@ -112,7 +112,7 @@
subsubsection {* Term cartouche and regular quotes *}
ML {*
- Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
+ Outer_Syntax.command @{command_spec "term_cartouche"} ""
(Parse.inner_syntax Parse.cartouche >> (fn s =>
Toplevel.keep (fn state =>
let
--- a/src/Provers/classical.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Provers/classical.ML Mon Nov 03 14:50:27 2014 +0100
@@ -980,7 +980,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
+ Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
end;
--- a/src/Pure/Isar/calculation.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/calculation.ML Mon Nov 03 14:50:27 2014 +0100
@@ -222,7 +222,7 @@
(Scan.succeed (Toplevel.proof' ultimately));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+ Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Nov 03 14:50:27 2014 +0100
@@ -397,7 +397,7 @@
(Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_bundles"}
+ Outer_Syntax.command @{command_spec "print_bundles"}
"print bundles of declarations"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
@@ -727,194 +727,194 @@
val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
val _ =
- Outer_Syntax.improper_command @{command_spec "help"}
+ Outer_Syntax.command @{command_spec "help"}
"retrieve outer syntax commands according to name patterns"
(Scan.repeat Parse.name >>
(fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_syntax pats)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
+ Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
(Scan.succeed (Toplevel.imperative Outer_Syntax.print_syntax));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_options"} "print configuration options"
+ Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_context"}
+ Outer_Syntax.command @{command_spec "print_context"}
"print context of local theory target"
(Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_theory"}
+ Outer_Syntax.command @{command_spec "print_theory"}
"print logical theory contents (verbose!)"
(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"}
+ Outer_Syntax.command @{command_spec "print_syntax"}
"print inner syntax of context (verbose!)"
(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"}
+ Outer_Syntax.command @{command_spec "print_defn_rules"}
"print definitional rewrite rules of context"
(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"}
+ Outer_Syntax.command @{command_spec "print_abbrevs"}
"print constant abbreviations of context"
(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"}
+ Outer_Syntax.command @{command_spec "print_theorems"}
"print theorems of local theory or proof context"
(opt_bang >> (fn b =>
Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_locales"}
+ Outer_Syntax.command @{command_spec "print_locales"}
"print locales of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_classes"}
+ Outer_Syntax.command @{command_spec "print_classes"}
"print classes of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Class.print_classes o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_locale"}
+ Outer_Syntax.command @{command_spec "print_locale"}
"print locale of this theory"
(opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
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"}
+ Outer_Syntax.command @{command_spec "print_interps"}
"print interpretations of locale for this theory or proof context"
(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"}
+ Outer_Syntax.command @{command_spec "print_dependencies"}
"print dependencies of locale expression"
(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"}
+ Outer_Syntax.command @{command_spec "print_attributes"}
"print attributes of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_simpset"}
+ Outer_Syntax.command @{command_spec "print_simpset"}
"print context of Simplifier"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
+ Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
+ Outer_Syntax.command @{command_spec "print_methods"} "print methods of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
+ Outer_Syntax.command @{command_spec "print_antiquotations"}
"print document antiquotations"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
+ Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
"print ML antiquotations"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
+ Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
(Scan.succeed Isar_Cmd.thy_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
+ Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
(Scan.succeed Isar_Cmd.locale_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
+ Outer_Syntax.command @{command_spec "print_term_bindings"}
"print term bindings of proof context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep
(Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
+ Outer_Syntax.command @{command_spec "print_facts"} "print facts of proof context"
(opt_bang >> (fn verbose => Toplevel.unknown_context o
Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
+ Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_statement"}
+ Outer_Syntax.command @{command_spec "print_statement"}
"print theorems as long statements"
(opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
val _ =
- Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
+ Outer_Syntax.command @{command_spec "thm"} "print theorems"
(opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
val _ =
- Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
+ Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
(opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
val _ =
- Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
+ Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
(opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
val _ =
- Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
+ Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
(opt_modes -- Parse.term >> Isar_Cmd.print_prop);
val _ =
- Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
+ Outer_Syntax.command @{command_spec "term"} "read and print term"
(opt_modes -- Parse.term >> Isar_Cmd.print_term);
val _ =
- Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
+ Outer_Syntax.command @{command_spec "typ"} "read and print type"
(opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
>> Isar_Cmd.print_type);
val _ =
- Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
+ Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_state"}
+ Outer_Syntax.command @{command_spec "print_state"}
"print current proof state (if present)"
(opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
val _ =
- Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
+ Outer_Syntax.command @{command_spec "welcome"} "print welcome message"
(Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
val _ =
- Outer_Syntax.improper_command @{command_spec "display_drafts"}
+ Outer_Syntax.command @{command_spec "display_drafts"}
"display raw source files with symbols"
(Scan.repeat1 Parse.path >> (fn names =>
Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
--- a/src/Pure/Isar/outer_syntax.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Nov 03 14:50:27 2014 +0100
@@ -19,8 +19,6 @@
(Toplevel.transition -> Toplevel.transition) parser -> unit
val markup_command: Thy_Output.markup -> command_spec -> string ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val improper_command: command_spec -> string ->
- (Toplevel.transition -> Toplevel.transition) parser -> unit
val local_theory': command_spec -> string ->
(bool -> local_theory -> local_theory) parser -> unit
val local_theory: command_spec -> string ->
@@ -50,14 +48,12 @@
datatype command = Command of
{comment: string,
markup: Thy_Output.markup option,
- int_only: bool,
parse: (Toplevel.transition -> Toplevel.transition) parser,
pos: Position.T,
id: serial};
-fun new_command comment markup int_only parse pos =
- Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
- pos = pos, id = serial ()};
+fun new_command comment markup parse pos =
+ Command {comment = comment, markup = markup, parse = parse, pos = pos, id = serial ()};
fun command_markup def (name, Command {pos, id, ...}) =
Markup.properties (Position.entity_properties_of def id pos)
@@ -153,13 +149,10 @@
end;
fun command (spec, pos) comment parse =
- add_command spec (new_command comment NONE false parse pos);
+ add_command spec (new_command comment NONE parse pos);
fun markup_command markup (spec, pos) comment parse =
- add_command spec (new_command comment (SOME markup) false parse pos);
-
-fun improper_command (spec, pos) comment parse =
- add_command spec (new_command comment NONE true parse pos);
+ add_command spec (new_command comment (SOME markup) parse pos);
end;
@@ -185,14 +178,11 @@
fun print_syntax () =
let
- val ((keywords, _), syntax) =
- CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
- val (int_cmds, cmds) =
- List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands syntax);
+ val ((keywords, _), syntax) = CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
+ val commands = dest_commands syntax;
in
[Pretty.strs ("syntax keywords:" :: map quote keywords),
- Pretty.big_list "commands:" (map pretty_command cmds),
- Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
+ Pretty.big_list "commands:" (map pretty_command commands)]
|> Pretty.writeln_chunks
end;
@@ -210,8 +200,7 @@
val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
in
(case lookup_commands syntax name of
- SOME (Command {int_only, parse, ...}) =>
- Parse.!!! (Parse.tags |-- parse) >> (fn f => tr0 |> Toplevel.interactive int_only |> f)
+ SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
| NONE =>
Scan.succeed
(tr0 |> Toplevel.imperative (fn () =>
--- a/src/Pure/Isar/toplevel.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Nov 03 14:50:27 2014 +0100
@@ -34,7 +34,6 @@
val type_error: transition -> state -> string
val name: string -> transition -> transition
val position: Position.T -> transition -> transition
- val interactive: bool -> transition -> transition
val init_theory: (unit -> theory) -> transition -> transition
val is_init: transition -> bool
val modify_init: (unit -> theory) -> transition -> transition
@@ -295,18 +294,16 @@
datatype transition = Transition of
{name: string, (*command name*)
pos: Position.T, (*source position*)
- int_only: bool, (*interactive-only*) (* TTY / Proof General legacy*)
timing: Time.time option, (*prescient timing information*)
trans: trans list}; (*primitive transitions (union)*)
-fun make_transition (name, pos, int_only, timing, trans) =
- Transition {name = name, pos = pos, int_only = int_only,
- timing = timing, trans = trans};
+fun make_transition (name, pos, timing, trans) =
+ Transition {name = name, pos = pos, timing = timing, trans = trans};
-fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
- make_transition (f (name, pos, int_only, timing, trans));
+fun map_transition f (Transition {name, pos, timing, trans}) =
+ make_transition (f (name, pos, timing, trans));
-val empty = make_transition ("", Position.none, false, NONE, []);
+val empty = make_transition ("", Position.none, NONE, []);
(* diagnostics *)
@@ -323,20 +320,17 @@
(* modify transitions *)
-fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
- (name, pos, int_only, timing, trans));
+fun name name = map_transition (fn (_, pos, timing, trans) =>
+ (name, pos, timing, trans));
-fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
- (name, pos, int_only, timing, trans));
+fun position pos = map_transition (fn (name, _, timing, trans) =>
+ (name, pos, timing, trans));
-fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
- (name, pos, int_only, timing, trans));
+fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
+ (name, pos, timing, tr :: trans));
-fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
- (name, pos, int_only, timing, tr :: trans));
-
-val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
- (name, pos, int_only, timing, []));
+val reset_trans = map_transition (fn (name, pos, timing, _) =>
+ (name, pos, timing, []));
(* basic transitions *)
@@ -559,8 +553,7 @@
(* apply transitions *)
fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
- (name, pos, int_only, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans));
local
--- a/src/Pure/Tools/class_deps.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML Mon Nov 03 14:50:27 2014 +0100
@@ -37,7 +37,7 @@
val visualize_cmd = gen_visualize Syntax.read_sort;
val _ =
- Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
+ Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
--- a/src/Pure/Tools/find_consts.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML Mon Nov 03 14:50:27 2014 +0100
@@ -149,7 +149,7 @@
|> #1;
val _ =
- Outer_Syntax.improper_command @{command_spec "find_consts"}
+ Outer_Syntax.command @{command_spec "find_consts"}
"find constants by name / type patterns"
(query >> (fn spec =>
Toplevel.keep (fn st =>
--- a/src/Pure/Tools/find_theorems.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Mon Nov 03 14:50:27 2014 +0100
@@ -535,7 +535,7 @@
|> #1;
val _ =
- Outer_Syntax.improper_command @{command_spec "find_theorems"}
+ Outer_Syntax.command @{command_spec "find_theorems"}
"find theorems meeting specified criteria"
(options -- query >> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.keep (fn st =>
--- a/src/Pure/Tools/thm_deps.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Tools/thm_deps.ML Mon Nov 03 14:50:27 2014 +0100
@@ -45,7 +45,7 @@
in Graph_Display.display_graph (sort_wrt #ID deps) end;
val _ =
- Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
+ Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
(Parse.xthms1 >> (fn args =>
Toplevel.unknown_theory o Toplevel.keep (fn state =>
thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
@@ -102,7 +102,7 @@
in rev thms' end;
val _ =
- Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
+ Outer_Syntax.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))) >> (fn opt_range =>
Toplevel.keep (fn state =>
--- a/src/Tools/Code/code_preproc.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML Mon Nov 03 14:50:27 2014 +0100
@@ -584,7 +584,7 @@
end;
val _ =
- Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
+ Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
(Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
end; (*struct*)
--- a/src/Tools/Code/code_thingol.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Nov 03 14:50:27 2014 +0100
@@ -939,14 +939,14 @@
in
val _ =
- Outer_Syntax.improper_command @{command_spec "code_thms"}
+ Outer_Syntax.command @{command_spec "code_thms"}
"print system of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.unknown_context o
Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
val _ =
- Outer_Syntax.improper_command @{command_spec "code_deps"}
+ Outer_Syntax.command @{command_spec "code_deps"}
"visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.unknown_context o
--- a/src/Tools/induct.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/induct.ML Mon Nov 03 14:50:27 2014 +0100
@@ -257,7 +257,7 @@
end;
val _ =
- Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
+ Outer_Syntax.command @{command_spec "print_induct_rules"}
"print induction and cases rules"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_rules o Toplevel.context_of)));
--- a/src/Tools/quickcheck.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/quickcheck.ML Mon Nov 03 14:50:27 2014 +0100
@@ -534,7 +534,7 @@
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
val _ =
- Outer_Syntax.improper_command @{command_spec "quickcheck"}
+ Outer_Syntax.command @{command_spec "quickcheck"}
"try to find counterexample for subgoal"
(parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
--- a/src/Tools/solve_direct.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/solve_direct.ML Mon Nov 03 14:50:27 2014 +0100
@@ -93,7 +93,7 @@
val solve_direct = do_solve_direct Normal
val _ =
- Outer_Syntax.improper_command @{command_spec "solve_direct"}
+ Outer_Syntax.command @{command_spec "solve_direct"}
"try to solve conjectures directly with existing theorems"
(Scan.succeed (Toplevel.unknown_proof o
Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
--- a/src/Tools/subtyping.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/subtyping.ML Mon Nov 03 14:50:27 2014 +0100
@@ -1114,7 +1114,7 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command @{command_spec "print_coercions"}
+ Outer_Syntax.command @{command_spec "print_coercions"}
"print information about coercions"
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
--- a/src/Tools/try.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Tools/try.ML Mon Nov 03 14:50:27 2014 +0100
@@ -75,7 +75,7 @@
|> tap (fn NONE => writeln "Tried in vain." | _ => ())
val _ =
- Outer_Syntax.improper_command @{command_spec "try"}
+ Outer_Syntax.command @{command_spec "try"}
"try a combination of automatic proving and disproving tools"
(Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
--- a/src/ZF/Tools/typechk.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/ZF/Tools/typechk.ML Mon Nov 03 14:50:27 2014 +0100
@@ -125,7 +125,7 @@
"ZF type-checking");
val _ =
- Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
+ Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_tcset o Toplevel.context_of)));