--- a/NEWS Mon Apr 06 15:23:50 2015 +0200
+++ b/NEWS Mon Apr 06 23:24:45 2015 +0200
@@ -6,9 +6,9 @@
*** General ***
-* Local theory specifications may have a 'private' modifier to restrict
-name space accesses to the current local scope, as delimited by "context
-begin ... end". For example, this works like this:
+* Local theory specification commands may have a 'private' or
+'restricted' modifier to limit name space accesses to the local scope,
+as provided by some "context begin ... end" block. For example:
context
begin
@@ -407,6 +407,10 @@
* Goal.prove_multi is superseded by the fully general Goal.prove_common,
which also allows to specify a fork priority.
+* Antiquotation @{command_spec "COMMAND"} is superseded by
+@{command_keyword COMMAND} (usually without quotes and with PIDE
+markup). Minor INCOMPATIBILITY.
+
*** System ***
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Apr 06 23:24:45 2015 +0200
@@ -471,7 +471,7 @@
\end{matharray}
@{rail \<open>
- 'rail' (@{syntax string} | @{syntax cartouche})
+ 'rail' @{syntax text}
\<close>}
The @{antiquotation rail} antiquotation allows to include syntax
--- a/src/Doc/Isar_Ref/Spec.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Apr 06 23:24:45 2015 +0200
@@ -115,6 +115,7 @@
@{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
@{keyword_def "private"} \\
+ @{keyword_def "restricted"} \\
\end{matharray}
A local theory target is a specification context that is managed
@@ -161,12 +162,16 @@
(global) "end"} has a different meaning: it concludes the theory
itself (\secref{sec:begin-thy}).
- \item @{keyword "private"} may be given as a modifier to any local theory
- command (before the command keyword). This limits name space accesses to
- the current local scope, as determined by the enclosing @{command
- "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Neither a
- global theory nor a locale target have such a local scope by themselves:
- an extra unnamed context is required to use @{keyword "private"} here.
+ \item @{keyword "private"} or @{keyword "restricted"} may be given as
+ modifiers before any local theory command. This limits name space accesses
+ to the local scope, as determined by the enclosing @{command
+ "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
+ scope, a @{keyword "private"} name is inaccessible, and a @{keyword
+ "restricted"} name is only accessible with additional qualification.
+
+ Neither a global @{command theory} nor a @{command locale} target provides
+ a local scope by itself: an extra unnamed context is required to use
+ @{keyword "private"} or @{keyword "restricted"} here.
\item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
theory command specifies an immediate target, e.g.\ ``@{command
--- a/src/FOL/FOL.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/FOL/FOL.thy Mon Apr 06 23:24:45 2015 +0200
@@ -384,10 +384,13 @@
text {* Proper handling of non-atomic rule statements. *}
-definition "induct_forall(P) == \<forall>x. P(x)"
-definition "induct_implies(A, B) == A \<longrightarrow> B"
-definition "induct_equal(x, y) == x = y"
-definition "induct_conj(A, B) == A \<and> B"
+context
+begin
+
+restricted definition "induct_forall(P) == \<forall>x. P(x)"
+restricted definition "induct_implies(A, B) == A \<longrightarrow> B"
+restricted definition "induct_equal(x, y) == x = y"
+restricted definition "induct_conj(A, B) == A \<and> B"
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
unfolding atomize_all induct_forall_def .
@@ -406,9 +409,6 @@
lemmas induct_rulify_fallback =
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
-hide_const induct_forall induct_implies induct_equal induct_conj
-
-
text {* Method setup. *}
ML_file "~~/src/Tools/induct.ML"
@@ -427,6 +427,8 @@
declare case_split [cases type: o]
+end
+
ML_file "~~/src/Tools/case_product.ML"
--- a/src/HOL/Decision_Procs/approximation.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Mon Apr 06 23:24:45 2015 +0200
@@ -244,7 +244,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val _ =
- Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
+ Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
(opt_modes -- Parse.term
>> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
--- a/src/HOL/Extraction.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Extraction.thy Mon Apr 06 23:24:45 2015 +0200
@@ -34,8 +34,8 @@
True_implies_equals TrueE
lemmas [extraction_expand_def] =
- induct_forall_def induct_implies_def induct_equal_def induct_conj_def
- induct_true_def induct_false_def
+ HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
+ HOL.induct_true_def HOL.induct_false_def
datatype (plugins only: code extraction) sumbool = Left | Right
--- a/src/HOL/HOL.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/HOL.thy Mon Apr 06 23:24:45 2015 +0200
@@ -1365,44 +1365,35 @@
subsubsection {* Generic cases and induction *}
text {* Rule projections: *}
-
ML {*
structure Project_Rule = Project_Rule
(
val conjunct1 = @{thm conjunct1}
val conjunct2 = @{thm conjunct2}
val mp = @{thm mp}
-)
+);
*}
-definition induct_forall where
- "induct_forall P == \<forall>x. P x"
-
-definition induct_implies where
- "induct_implies A B == A \<longrightarrow> B"
-
-definition induct_equal where
- "induct_equal x y == x = y"
+context
+begin
-definition induct_conj where
- "induct_conj A B == A \<and> B"
+restricted definition "induct_forall P \<equiv> \<forall>x. P x"
+restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
+restricted definition "induct_equal x y \<equiv> x = y"
+restricted definition "induct_conj A B \<equiv> A \<and> B"
+restricted definition "induct_true \<equiv> True"
+restricted definition "induct_false \<equiv> False"
-definition induct_true where
- "induct_true == True"
-
-definition induct_false where
- "induct_false == False"
-
-lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
+lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
by (unfold atomize_all induct_forall_def)
-lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
+lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)"
by (unfold atomize_imp induct_implies_def)
-lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
+lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)"
by (unfold atomize_eq induct_equal_def)
-lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
+lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)"
by (unfold atomize_conj induct_conj_def)
lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
@@ -1413,7 +1404,6 @@
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_true_def induct_false_def
-
lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
induct_conj (induct_forall A) (induct_forall B)"
by (unfold induct_forall_def induct_conj_def) iprover
@@ -1422,13 +1412,15 @@
induct_conj (induct_implies C A) (induct_implies C B)"
by (unfold induct_implies_def induct_conj_def) iprover
-lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
+lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)"
proof
- assume r: "induct_conj A B ==> PROP C" and A B
- show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`)
+ assume r: "induct_conj A B \<Longrightarrow> PROP C"
+ assume ab: A B
+ show "PROP C" by (rule r) (simp add: induct_conj_def ab)
next
- assume r: "A ==> B ==> PROP C" and "induct_conj A B"
- show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def])
+ assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C"
+ assume ab: "induct_conj A B"
+ show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def])
qed
lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
@@ -1455,8 +1447,8 @@
ML_file "~~/src/Tools/induction.ML"
-setup {*
- Context.theory_map (Induct.map_simpset (fn ss => ss
+declaration {*
+ fn _ => Induct.map_simpset (fn ss => ss
addsimprocs
[Simplifier.simproc_global @{theory} "swap_induct_false"
["induct_false ==> PROP P ==> PROP Q"]
@@ -1479,60 +1471,62 @@
| _ => NONE))]
|> Simplifier.set_mksimps (fn ctxt =>
Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
- map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
+ map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
*}
text {* Pre-simplification of induction and cases rules *}
-lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t"
+lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
unfolding induct_equal_def
proof
- assume R: "!!x. x = t ==> PROP P x"
- show "PROP P t" by (rule R [OF refl])
+ assume r: "\<And>x. x = t \<Longrightarrow> PROP P x"
+ show "PROP P t" by (rule r [OF refl])
next
- fix x assume "PROP P t" "x = t"
+ fix x
+ assume "PROP P t" "x = t"
then show "PROP P x" by simp
qed
-lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t"
+lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
unfolding induct_equal_def
proof
- assume R: "!!x. t = x ==> PROP P x"
- show "PROP P t" by (rule R [OF refl])
+ assume r: "\<And>x. t = x \<Longrightarrow> PROP P x"
+ show "PROP P t" by (rule r [OF refl])
next
- fix x assume "PROP P t" "t = x"
+ fix x
+ assume "PROP P t" "t = x"
then show "PROP P x" by simp
qed
-lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true"
+lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true"
unfolding induct_false_def induct_true_def
by (iprover intro: equal_intr_rule)
-lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P"
+lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P"
unfolding induct_true_def
proof
- assume R: "True \<Longrightarrow> PROP P"
- from TrueI show "PROP P" by (rule R)
+ assume "True \<Longrightarrow> PROP P"
+ then show "PROP P" using TrueI .
next
assume "PROP P"
then show "PROP P" .
qed
-lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true"
+lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true"
unfolding induct_true_def
by (iprover intro: equal_intr_rule)
-lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true"
+lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
unfolding induct_true_def
by (iprover intro: equal_intr_rule)
-lemma [induct_simp]: "induct_implies induct_true P == P"
+lemma [induct_simp]: "induct_implies induct_true P \<equiv> P"
by (simp add: induct_implies_def induct_true_def)
-lemma [induct_simp]: "(x = x) = True"
+lemma [induct_simp]: "x = x \<longleftrightarrow> True"
by (rule simp_thms)
-hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
+end
ML_file "~~/src/Tools/induct_tacs.ML"
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Apr 06 23:24:45 2015 +0200
@@ -261,7 +261,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
+ Outer_Syntax.command @{command_keyword domain} "define recursive domains (HOLCF)"
(domains_decl >> (Toplevel.theory o mk_domain))
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Apr 06 23:24:45 2015 +0200
@@ -755,7 +755,7 @@
in
val _ =
- Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
+ Outer_Syntax.command @{command_keyword domain_isomorphism} "define domain isomorphisms (HOLCF)"
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
end
--- a/src/HOL/HOLCF/Tools/cpodef.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Mon Apr 06 23:24:45 2015 +0200
@@ -332,12 +332,12 @@
((t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command @{command_spec "pcpodef"}
+ Outer_Syntax.command @{command_keyword pcpodef}
"HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
val _ =
- Outer_Syntax.command @{command_spec "cpodef"}
+ Outer_Syntax.command @{command_keyword cpodef}
"HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
--- a/src/HOL/HOLCF/Tools/domaindef.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Mon Apr 06 23:24:45 2015 +0200
@@ -209,7 +209,7 @@
domaindef_cmd ((t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
+ Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations"
(domaindef_decl >> (Toplevel.theory o mk_domaindef))
end
--- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Apr 06 23:24:45 2015 +0200
@@ -399,7 +399,7 @@
in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
val _ =
- Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
+ Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
(Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
>> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
--- a/src/HOL/Import/import_data.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Import/import_data.ML Mon Apr 06 23:24:45 2015 +0200
@@ -117,13 +117,13 @@
"declare a type_definition theorem as a map for an imported type with abs and rep")
val _ =
- Outer_Syntax.command @{command_spec "import_type_map"}
+ Outer_Syntax.command @{command_keyword import_type_map}
"map external type name to existing Isabelle/HOL type name"
((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
(fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
val _ =
- Outer_Syntax.command @{command_spec "import_const_map"}
+ Outer_Syntax.command @{command_keyword import_const_map}
"map external const name to existing Isabelle/HOL const name"
((Parse.name --| @{keyword ":"}) -- Parse.const >>
(fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
--- a/src/HOL/Import/import_rule.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Mon Apr 06 23:24:45 2015 +0200
@@ -444,7 +444,7 @@
fun process_file path thy =
(thy, init_state) |> File.fold_lines process_line path |> fst
-val _ = Outer_Syntax.command @{command_spec "import_file"}
+val _ = Outer_Syntax.command @{command_keyword import_file}
"import a recorded proof file"
(Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML Mon Apr 06 23:24:45 2015 +0200
@@ -246,7 +246,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "old_smt_status"}
+ Outer_Syntax.command @{command_keyword 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/bnf_axiomatization.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Mon Apr 06 23:24:45 2015 +0200
@@ -118,7 +118,7 @@
parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings;
val _ =
- Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
+ Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
(parse_bnf_axiomatization >>
(fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) =>
bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd));
--- a/src/HOL/Library/code_test.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Library/code_test.ML Mon Apr 06 23:24:45 2015 +0200
@@ -567,7 +567,7 @@
val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
val _ =
- Outer_Syntax.command @{command_spec "test_code"}
+ Outer_Syntax.command @{command_keyword test_code}
"compile test cases to target languages, execute them and report results"
(test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
--- a/src/HOL/Library/refute.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Library/refute.ML Mon Apr 06 23:24:45 2015 +0200
@@ -2965,7 +2965,7 @@
(* 'refute' command *)
val _ =
- Outer_Syntax.command @{command_spec "refute"}
+ Outer_Syntax.command @{command_keyword refute}
"try to find a model that refutes a given subgoal"
(scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
@@ -2980,7 +2980,7 @@
(* 'refute_params' command *)
val _ =
- Outer_Syntax.command @{command_spec "refute_params"}
+ Outer_Syntax.command @{command_keyword refute_params}
"show/store default parameters for the 'refute' command"
(scan_parms >> (fn parms =>
Toplevel.theory (fn thy =>
--- a/src/HOL/Library/simps_case_conv.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML Mon Apr 06 23:24:45 2015 +0200
@@ -219,7 +219,7 @@
end
val _ =
- Outer_Syntax.local_theory @{command_spec "case_of_simps"}
+ Outer_Syntax.local_theory @{command_keyword case_of_simps}
"turn a list of equations into a case expression"
(Parse_Spec.opt_thm_name ":" -- Parse.xthms1 >> case_of_simps_cmd)
@@ -227,7 +227,7 @@
Parse.xthms1 --| @{keyword ")"}
val _ =
- Outer_Syntax.local_theory @{command_spec "simps_of_case"}
+ Outer_Syntax.local_theory @{command_keyword simps_of_case}
"perform case split on rule"
(Parse_Spec.opt_thm_name ":" -- Parse.xthm --
Scan.optional parse_splits [] >> simps_of_case_cmd)
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Apr 06 23:24:45 2015 +0200
@@ -247,10 +247,10 @@
end
val forbidden_mutant_constnames =
- ["HOL.induct_equal",
- "HOL.induct_implies",
- "HOL.induct_conj",
- "HOL.induct_forall",
+[@{const_name HOL.induct_equal},
+ @{const_name HOL.induct_implies},
+ @{const_name HOL.induct_conj},
+ @{const_name HOL.induct_forall},
@{const_name undefined},
@{const_name default},
@{const_name Pure.dummy_pattern},
--- a/src/HOL/Nominal/Nominal.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy Mon Apr 06 23:24:45 2015 +0200
@@ -3563,7 +3563,7 @@
(* connectives *)
if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt
true_eqvt false_eqvt
- imp_eqvt [folded induct_implies_def]
+ imp_eqvt [folded HOL.induct_implies_def]
(* datatypes *)
perm_unit.simps
--- a/src/HOL/Nominal/nominal_atoms.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Apr 06 23:24:45 2015 +0200
@@ -28,7 +28,7 @@
val finite_emptyI = @{thm "finite.emptyI"};
val Collect_const = @{thm "Collect_const"};
-val inductive_forall_def = @{thm "induct_forall_def"};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
(* theory data *)
@@ -1018,7 +1018,7 @@
(* syntax und parsing *)
val _ =
- Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
+ Outer_Syntax.command @{command_keyword atom_decl} "declare new kinds of atoms"
(Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Apr 06 23:24:45 2015 +0200
@@ -2074,7 +2074,7 @@
val nominal_datatype_cmd = gen_nominal_datatype Old_Datatype.read_specs;
val _ =
- Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
+ Outer_Syntax.command @{command_keyword nominal_datatype} "define nominal datatypes"
(Parse.and_list1 Old_Datatype.spec_cmd >>
(Toplevel.theory o nominal_datatype_cmd Old_Datatype_Aux.default_config));
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 23:24:45 2015 +0200
@@ -14,7 +14,7 @@
structure NominalInductive : NOMINAL_INDUCTIVE =
struct
-val inductive_forall_def = @{thm induct_forall_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
val inductive_atomize = @{thms induct_atomize};
val inductive_rulify = @{thms induct_rulify};
@@ -671,14 +671,14 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive}
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
(Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
(@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
- Outer_Syntax.local_theory @{command_spec "equivariance"}
+ Outer_Syntax.local_theory @{command_keyword equivariance}
"prove equivariance for inductive predicate involving nominal datatypes"
(Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Apr 06 23:24:45 2015 +0200
@@ -15,7 +15,7 @@
structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
struct
-val inductive_forall_def = @{thm induct_forall_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
val inductive_atomize = @{thms induct_atomize};
val inductive_rulify = @{thms induct_rulify};
@@ -483,7 +483,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive2}
"prove strong induction theorem for inductive predicate involving nominal datatypes"
(Parse.xname --
Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
--- a/src/HOL/Nominal/nominal_primrec.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon Apr 06 23:24:45 2015 +0200
@@ -403,7 +403,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
"define primitive recursive functions on nominal datatypes"
(options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>
--- a/src/HOL/Orderings.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Orderings.thy Mon Apr 06 23:24:45 2015 +0200
@@ -439,7 +439,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_orders"}
+ Outer_Syntax.command @{command_keyword 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/SMT_Examples/boogie.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML Mon Apr 06 23:24:45 2015 +0200
@@ -266,7 +266,7 @@
(* Isar command *)
val _ =
- Outer_Syntax.command @{command_spec "boogie_file"}
+ Outer_Syntax.command @{command_keyword boogie_file}
"prove verification condition from .b2i file"
(Resources.provide_parse_files "boogie_file" >> (fn files =>
Toplevel.theory (fn thy =>
--- a/src/HOL/SPARK/Manual/Reference.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy Mon Apr 06 23:24:45 2015 +0200
@@ -23,7 +23,9 @@
\label{sec:spark-commands}
This section describes the syntax and effect of each of the commands provided
by HOL-\SPARK{}.
-@{rail "@'spark_open' name ('(' name ')')?"}
+@{rail \<open>
+ @'spark_open' name ('(' name ')')?
+\<close>}
Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
The corresponding \texttt{*.fdl} and \texttt{*.rls}
@@ -36,7 +38,9 @@
format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
packages, this is necessary in order for the verification environment to be able to map proof
functions and types defined in Isabelle to their \SPARK{} counterparts.
-@{rail "@'spark_proof_functions' ((name '=' term)+)"}
+@{rail \<open>
+ @'spark_proof_functions' ((name '=' term)+)
+\<close>}
Associates a proof function with the given name to a term. The name should be the full name
of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
This command can be used both inside and outside a verification environment. The latter
@@ -44,8 +48,11 @@
or packages, whereas the former allows the given term to refer to the types generated
by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
\texttt{*.fdl} file.
-@{rail "@'spark_types' ((name '=' type (mapping?))+);
-mapping: '('((name '=' nameref)+',')')'"}
+@{rail \<open>
+ @'spark_types' ((name '=' type (mapping?))+)
+ ;
+ mapping: '('((name '=' nameref)+',')')'
+\<close>}
Associates a \SPARK{} type with the given name with an Isabelle type. This command can
only be used outside a verification environment. The given type must be either a record
or a datatype, where the names of fields or constructors must either match those of the
@@ -57,18 +64,24 @@
using Isabelle's commands for defining records or datatypes. Having introduced the
types, the proof functions can be defined in Isabelle. Finally, both the proof
functions and the types can be associated with their \SPARK{} counterparts.
-@{rail "@'spark_status' (('(proved)' | '(unproved)')?)"}
+@{rail \<open>
+ @'spark_status' (('(proved)' | '(unproved)')?)
+\<close>}
Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
The output can be restricted to the proved or unproved VCs by giving the corresponding
option to the command.
-@{rail "@'spark_vc' name"}
+@{rail \<open>
+ @'spark_vc' name
+\<close>}
Initiates the proof of the VC with the given name. Similar to the standard
\isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
must be followed by a sequence of proof commands. The command introduces the
hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
\texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
-@{rail "@'spark_end' '(incomplete)'?"}
+@{rail \<open>
+ @'spark_end' '(incomplete)'?
+\<close>}
Closes the current verification environment. Unless the \texttt{incomplete}
option is given, all VCs must have been proved,
otherwise the command issues an error message. As a side effect, the command
--- a/src/HOL/SPARK/Tools/spark_commands.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Mon Apr 06 23:24:45 2015 +0200
@@ -92,13 +92,13 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "spark_open_vcg"}
+ Outer_Syntax.command @{command_keyword spark_open_vcg}
"open a new SPARK environment and load a SPARK-generated .vcg file"
(Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
val _ =
- Outer_Syntax.command @{command_spec "spark_open"}
+ Outer_Syntax.command @{command_keyword spark_open}
"open a new SPARK environment and load a SPARK-generated .siv file"
(Resources.provide_parse_files "spark_open" -- Parse.parname
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
@@ -107,13 +107,13 @@
(Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
val _ =
- Outer_Syntax.command @{command_spec "spark_proof_functions"}
+ Outer_Syntax.command @{command_keyword spark_proof_functions}
"associate SPARK proof functions with terms"
(Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
(Toplevel.theory o fold add_proof_fun_cmd));
val _ =
- Outer_Syntax.command @{command_spec "spark_types"}
+ Outer_Syntax.command @{command_keyword spark_types}
"associate SPARK types with types"
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
Scan.optional (Args.parens (Parse.list1
@@ -121,12 +121,12 @@
(Toplevel.theory o fold add_spark_type_cmd));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "spark_vc"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc}
"enter into proof mode for a specific verification condition"
(Parse.name >> prove_vc);
val _ =
- Outer_Syntax.command @{command_spec "spark_status"}
+ Outer_Syntax.command @{command_keyword spark_status}
"show the name and state of all loaded verification conditions"
(Scan.optional
(Args.parens
@@ -136,7 +136,7 @@
Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args)))
val _ =
- Outer_Syntax.command @{command_spec "spark_end"}
+ Outer_Syntax.command @{command_keyword spark_end}
"close the current SPARK environment"
(Scan.optional (@{keyword "("} |-- Parse.!!!
(Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
--- a/src/HOL/Statespace/state_space.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon Apr 06 23:24:45 2015 +0200
@@ -650,7 +650,7 @@
(plus1_unless comp parent --
Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
val _ =
- Outer_Syntax.command @{command_spec "statespace"} "define state-space as locale context"
+ Outer_Syntax.command @{command_keyword statespace} "define state-space as locale context"
(statespace_decl >> (fn ((args, name), (parents, comps)) =>
Toplevel.theory (define_statespace args name parents comps)));
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Apr 06 23:24:45 2015 +0200
@@ -912,7 +912,7 @@
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
- Outer_Syntax.command @{command_spec "import_tptp"} "import TPTP problem"
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1854,7 +1854,7 @@
(*This has been disabled since it requires a hook to be specified to use "import_thm"
val _ =
- Outer_Syntax.command @{command_spec "import_leo2_proof"} "import TPTP proof"
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1615,12 +1615,12 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_bnfs"}
+ Outer_Syntax.command @{command_keyword print_bnfs}
"print all bounded natural functors"
(Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword bnf}
"register a type as a bounded natural functor"
(parse_opt_binding_colon -- Parse.typ --|
(Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 06 23:24:45 2015 +0200
@@ -2019,7 +2019,7 @@
val fake_T = qsoty (unfreeze_fp X);
val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
fun register_hint () =
- "\nUse the " ^ quote (#1 @{command_spec "bnf"}) ^ " command to register " ^
+ "\nUse the " ^ quote (#1 @{command_keyword bnf}) ^ " command to register " ^
quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \
\it";
in
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Apr 06 23:24:45 2015 +0200
@@ -2555,7 +2555,7 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
+ Outer_Syntax.local_theory @{command_keyword codatatype} "define coinductive datatypes"
(parse_co_datatype_cmd Greatest_FP construct_gfp);
val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Apr 06 23:24:45 2015 +0200
@@ -112,8 +112,8 @@
fun unexpected_corec_call ctxt eqns t =
error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
fun use_primcorecursive () =
- error ("\"auto\" failed (try " ^ quote (#1 @{command_spec "primcorecursive"}) ^ " instead of " ^
- quote (#1 @{command_spec "primcorec"}) ^ ")");
+ error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
+ quote (#1 @{command_keyword primcorec}) ^ ")");
datatype corec_option =
Plugins_Option of Proof.context -> Plugin_Name.filter |
@@ -1551,13 +1551,13 @@
val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
-val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
+val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
"define primitive corecursive functions"
((Scan.optional (@{keyword "("} |--
Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
(Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
-val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
+val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
"define primitive corecursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
--| @{keyword ")"}) []) --
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1842,7 +1842,7 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
+ Outer_Syntax.local_theory @{command_keyword datatype} "define inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Apr 06 23:24:45 2015 +0200
@@ -539,7 +539,7 @@
BNF_LFP_Rec_Sugar.add_primrec_simple;
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype_compat"}
+ Outer_Syntax.local_theory @{command_keyword datatype_compat}
"register datatypes as old-style datatypes and derive old-style properties"
(Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Apr 06 23:24:45 2015 +0200
@@ -669,7 +669,7 @@
|| Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
|| Parse.reserved "transfer" >> K Transfer_Option);
-val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
+val _ = Outer_Syntax.local_theory @{command_keyword primrec}
"define primitive recursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
--| @{keyword ")"}) []) --
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Mon Apr 06 23:24:45 2015 +0200
@@ -630,7 +630,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_case_translations"}
+ Outer_Syntax.command @{command_keyword print_case_translations}
"print registered case combinators and constructors"
(Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1143,7 +1143,7 @@
val parse_sel_default_eqs = Scan.optional (@{keyword "where"} |-- Parse.enum1 "|" Parse.prop) [];
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword free_constructors}
"register an existing freely generated type's constructors"
(parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
-- parse_sel_default_eqs
--- a/src/HOL/Tools/Function/fun.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Function/fun.ML Mon Apr 06 23:24:45 2015 +0200
@@ -172,7 +172,7 @@
val _ =
- Outer_Syntax.local_theory' @{command_spec "fun"}
+ Outer_Syntax.local_theory' @{command_keyword fun}
"define general recursive functions (short version)"
(function_parser fun_config
>> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
--- a/src/HOL/Tools/Function/fun_cases.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Apr 06 23:24:45 2015 +0200
@@ -54,7 +54,7 @@
val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
val _ =
- Outer_Syntax.local_theory @{command_spec "fun_cases"}
+ Outer_Syntax.local_theory @{command_keyword fun_cases}
"create simplified instances of elimination rules for function equations"
(Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
--- a/src/HOL/Tools/Function/function.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Apr 06 23:24:45 2015 +0200
@@ -286,13 +286,13 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
+ Outer_Syntax.local_theory_to_proof' @{command_keyword function}
"define general recursive functions"
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword termination}
"prove termination of a recursive function"
(Scan.option Parse.term >> termination_cmd)
--- a/src/HOL/Tools/Function/partial_function.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon Apr 06 23:24:45 2015 +0200
@@ -309,7 +309,7 @@
val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
val _ =
- Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
+ Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
>> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 06 23:24:45 2015 +0200
@@ -700,7 +700,7 @@
--| @{keyword "is"} -- Parse.term --
Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition}
"definition for constants over the quotient type"
(liftdef_parser >> lift_def_cmd_with_err_handling)
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Apr 06 23:24:45 2015 +0200
@@ -533,11 +533,11 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.command @{command_spec "print_quot_maps"} "print quotient map functions"
+ Outer_Syntax.command @{command_keyword print_quot_maps} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
val _ =
- Outer_Syntax.command @{command_spec "print_quotients"} "print quotients"
+ Outer_Syntax.command @{command_keyword print_quotients} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Apr 06 23:24:45 2015 +0200
@@ -787,7 +787,7 @@
end
val _ =
- Outer_Syntax.local_theory @{command_spec "setup_lifting"}
+ Outer_Syntax.local_theory @{command_keyword setup_lifting}
"setup lifting infrastructure"
(Parse.xthm -- Scan.option Parse.xthm
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >>
@@ -998,7 +998,7 @@
val _ =
- Outer_Syntax.local_theory @{command_spec "lifting_forget"}
+ Outer_Syntax.local_theory @{command_keyword lifting_forget}
"unsetup Lifting and Transfer for the given lifting bundle"
(Parse.position Parse.xname >> (lifting_forget_cmd))
@@ -1027,7 +1027,7 @@
update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
val _ =
- Outer_Syntax.local_theory @{command_spec "lifting_update"}
+ Outer_Syntax.local_theory @{command_keyword lifting_update}
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
(Parse.position Parse.xname >> lifting_update_cmd)
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Mon Apr 06 23:24:45 2015 +0200
@@ -374,7 +374,7 @@
|> sort_strings |> cat_lines)))))
val _ =
- Outer_Syntax.command @{command_spec "nitpick"}
+ Outer_Syntax.command @{command_keyword 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
@@ -383,7 +383,7 @@
(Toplevel.proof_of state)))))
val _ =
- Outer_Syntax.command @{command_spec "nitpick_params"}
+ Outer_Syntax.command @{command_keyword nitpick_params}
"set and display the default parameters for Nitpick"
(parse_params #>> nitpick_params_trans)
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Apr 06 23:24:45 2015 +0200
@@ -788,7 +788,7 @@
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =
- Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
+ Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
(Parse.and_list1 spec_cmd
>> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Apr 06 23:24:45 2015 +0200
@@ -680,7 +680,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "old_rep_datatype"}
+ Outer_Syntax.command @{command_keyword old_rep_datatype}
"register existing types as old-style datatypes"
(Scan.repeat1 Parse.term >> (fn ts =>
Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1033,7 +1033,7 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
val _ =
- Outer_Syntax.command @{command_spec "values_prolog"}
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Apr 06 23:24:45 2015 +0200
@@ -278,12 +278,12 @@
(* code_pred command and values command *)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword code_pred}
"prove equations for predicate specified by intro/elim rules"
(opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
val _ =
- Outer_Syntax.command @{command_spec "values"}
+ Outer_Syntax.command @{command_keyword 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/abstract_generators.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Mon Apr 06 23:24:45 2015 +0200
@@ -67,7 +67,7 @@
Syntax.read_term
val _ =
- Outer_Syntax.command @{command_spec "quickcheck_generator"}
+ Outer_Syntax.command @{command_keyword quickcheck_generator}
"define quickcheck generators for abstract types"
((Parse.type_const --
Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Apr 06 23:24:45 2015 +0200
@@ -111,7 +111,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "find_unused_assms"}
+ Outer_Syntax.command @{command_keyword 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_def.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 06 23:24:45 2015 +0200
@@ -213,7 +213,7 @@
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword quotient_definition}
"definition for constants over the quotient type"
(quotdef_parser >> quotient_def_cmd)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon Apr 06 23:24:45 2015 +0200
@@ -229,15 +229,15 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
+ Outer_Syntax.command @{command_keyword print_quotmapsQ3} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
val _ =
- Outer_Syntax.command @{command_spec "print_quotientsQ3"} "print quotients"
+ Outer_Syntax.command @{command_keyword print_quotientsQ3} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
val _ =
- Outer_Syntax.command @{command_spec "print_quotconsts"} "print quotient constants"
+ Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
end;
--- a/src/HOL/Tools/Quotient/quotient_type.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Mon Apr 06 23:24:45 2015 +0200
@@ -342,7 +342,7 @@
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
"quotient type definitions (require equivalence proofs)"
(quotspec_parser >> quotient_type_cmd)
--- a/src/HOL/Tools/SMT/smt_config.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Apr 06 23:24:45 2015 +0200
@@ -257,7 +257,7 @@
end
val _ =
- Outer_Syntax.command @{command_spec "smt_status"}
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Apr 06 23:24:45 2015 +0200
@@ -387,12 +387,12 @@
no_fact_override
val _ =
- Outer_Syntax.command @{command_spec "sledgehammer"}
+ Outer_Syntax.command @{command_keyword 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)
val _ =
- Outer_Syntax.command @{command_spec "sledgehammer_params"}
+ Outer_Syntax.command @{command_keyword sledgehammer_params}
"set and display the default parameters for Sledgehammer"
(parse_params #>> sledgehammer_params_trans)
--- a/src/HOL/Tools/choice_specification.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Apr 06 23:24:45 2015 +0200
@@ -198,7 +198,7 @@
val opt_overloaded = Parse.opt_keyword "overloaded"
val _ =
- Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
+ Outer_Syntax.command @{command_keyword specification} "define constants by specification"
(@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
>> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
--- a/src/HOL/Tools/functor.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/functor.ML Mon Apr 06 23:24:45 2015 +0200
@@ -273,7 +273,7 @@
val functor_cmd = gen_functor Syntax.read_term;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "functor"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword functor}
"register operations managing the functorial structure of a type"
(Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
>> (fn (prfx, t) => functor_cmd prfx t));
--- a/src/HOL/Tools/inductive.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Apr 06 23:24:45 2015 +0200
@@ -97,9 +97,8 @@
(** theory context references **)
-val inductive_forall_def = @{thm induct_forall_def};
-val inductive_conj_name = "HOL.induct_conj";
-val inductive_conj_def = @{thm induct_conj_def};
+val inductive_forall_def = @{thm HOL.induct_forall_def};
+val inductive_conj_def = @{thm HOL.induct_conj_def};
val inductive_conj = @{thms induct_conj};
val inductive_atomize = @{thms induct_atomize};
val inductive_rulify = @{thms induct_rulify};
@@ -689,7 +688,7 @@
val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
val Q =
fold_rev Term.abs (mk_names "x" k ~~ Ts)
- (HOLogic.mk_binop inductive_conj_name
+ (HOLogic.mk_binop @{const_name HOL.induct_conj}
(list_comb (incr_boundvars k s, bs), P));
in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
| NONE =>
@@ -1171,25 +1170,25 @@
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates"
+ Outer_Syntax.local_theory @{command_keyword inductive} "define inductive predicates"
(ind_decl false);
val _ =
- Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
+ Outer_Syntax.local_theory @{command_keyword coinductive} "define coinductive predicates"
(ind_decl true);
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive_cases"}
+ Outer_Syntax.local_theory @{command_keyword inductive_cases}
"create simplified instances of elimination rules"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive_simps"}
+ Outer_Syntax.local_theory @{command_keyword inductive_simps}
"create simplification rules for inductive predicates"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
val _ =
- Outer_Syntax.command @{command_spec "print_inductives"}
+ Outer_Syntax.command @{command_keyword print_inductives}
"print (co)inductive definitions and monotonicity rules"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (print_inductives b o Toplevel.context_of)));
--- a/src/HOL/Tools/inductive_set.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Apr 06 23:24:45 2015 +0200
@@ -568,11 +568,11 @@
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
val _ =
- Outer_Syntax.local_theory @{command_spec "inductive_set"} "define inductive sets"
+ Outer_Syntax.local_theory @{command_keyword inductive_set} "define inductive sets"
(ind_set_decl false);
val _ =
- Outer_Syntax.local_theory @{command_spec "coinductive_set"} "define coinductive sets"
+ Outer_Syntax.local_theory @{command_keyword coinductive_set} "define coinductive sets"
(ind_set_decl true);
end;
--- a/src/HOL/Tools/recdef.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/recdef.ML Mon Apr 06 23:24:45 2015 +0200
@@ -298,7 +298,7 @@
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
+ Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
(recdef_decl >> Toplevel.theory);
@@ -309,12 +309,12 @@
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
- Outer_Syntax.command @{command_spec "defer_recdef"}
+ Outer_Syntax.command @{command_keyword defer_recdef}
"defer general recursive functions (obsolete TFL)"
(defer_recdef_decl >> Toplevel.theory);
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
+ Outer_Syntax.local_theory_to_proof' @{command_keyword recdef_tc}
"recommence proof of termination condition (obsolete TFL)"
((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
--- a/src/HOL/Tools/record.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/record.ML Mon Apr 06 23:24:45 2015 +0200
@@ -2329,7 +2329,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "record"} "define extensible record"
+ Outer_Syntax.command @{command_keyword record} "define extensible record"
(Parse.type_args_constrained -- Parse.binding --
(@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
--- a/src/HOL/Tools/try0.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/try0.ML Mon Apr 06 23:24:45 2015 +0200
@@ -177,7 +177,7 @@
|| Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
val _ =
- Outer_Syntax.command @{command_spec "try0"} "try a combination of proof methods"
+ Outer_Syntax.command @{command_keyword 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/typedef.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Mon Apr 06 23:24:45 2015 +0200
@@ -281,7 +281,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
"HOL type definition (requires non-emptiness proof)"
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.term) --
--- a/src/HOL/Tools/value.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/Tools/value.ML Mon Apr 06 23:24:45 2015 +0200
@@ -70,7 +70,7 @@
Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
val _ =
- Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Apr 06 23:24:45 2015 +0200
@@ -40,7 +40,7 @@
subsection \<open>Outer syntax: cartouche within command syntax\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "cartouche"} ""
+ Outer_Syntax.command @{command_keyword cartouche} ""
(Parse.cartouche >> (fn s =>
Toplevel.imperative (fn () => writeln s)))
\<close>
@@ -116,7 +116,7 @@
subsubsection \<open>Term cartouche and regular quotes\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "term_cartouche"} ""
+ Outer_Syntax.command @{command_keyword term_cartouche} ""
(Parse.inner_syntax Parse.cartouche >> (fn s =>
Toplevel.keep (fn state =>
let
@@ -178,7 +178,7 @@
ML \<open>
Outer_Syntax.command
- @{command_spec "text_cartouche"} ""
+ @{command_keyword text_cartouche} ""
(Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
\<close>
--- a/src/HOL/ex/Commands.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/HOL/ex/Commands.thy Mon Apr 06 23:24:45 2015 +0200
@@ -15,7 +15,7 @@
subsection \<open>Diagnostic command: no state change\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "print_test"} "print term test"
+ Outer_Syntax.command @{command_keyword print_test} "print term test"
(Parse.term >> (fn s => Toplevel.keep (fn st =>
let
val ctxt = Toplevel.context_of st;
@@ -30,7 +30,7 @@
subsection \<open>Old-style global theory declaration\<close>
ML \<open>
- Outer_Syntax.command @{command_spec "global_test"} "test constant declaration"
+ Outer_Syntax.command @{command_keyword global_test} "test constant declaration"
(Parse.binding >> (fn b => Toplevel.theory (fn thy =>
let
val thy' = Sign.add_consts [(b, @{typ 'a}, NoSyn)] thy;
@@ -45,7 +45,7 @@
subsection \<open>Local theory specification\<close>
ML \<open>
- Outer_Syntax.local_theory @{command_spec "local_test"} "test local definition"
+ Outer_Syntax.local_theory @{command_keyword local_test} "test local definition"
(Parse.binding -- (@{keyword "="} |-- Parse.term) >> (fn (b, s) => fn lthy =>
let
val t = Syntax.read_term lthy s;
--- a/src/Provers/classical.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Provers/classical.ML Mon Apr 06 23:24:45 2015 +0200
@@ -974,7 +974,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.command @{command_spec "print_claset"} "print context of Classical Reasoner"
+ Outer_Syntax.command @{command_keyword 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/General/binding.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/General/binding.ML Mon Apr 06 23:24:45 2015 +0200
@@ -31,7 +31,8 @@
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
val private: scope -> binding -> binding
- val private_default: scope option -> binding -> binding
+ val restricted: scope -> binding -> binding
+ val limited_default: (bool * scope) option -> binding -> binding
val concealed: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
@@ -39,7 +40,7 @@
val bad: binding -> string
val check: binding -> unit
val name_spec: scope list -> (string * bool) list -> binding ->
- {accessible: bool, concealed: bool, spec: (string * bool) list}
+ {limitation: bool option, concealed: bool, spec: (string * bool) list}
end;
structure Binding: BINDING =
@@ -47,7 +48,7 @@
(** representation **)
-(* scope of private entries *)
+(* scope of limited entries *)
datatype scope = Scope of serial;
@@ -57,19 +58,19 @@
(* binding *)
datatype binding = Binding of
- {private: scope option, (*entry is strictly private within its scope*)
- concealed: bool, (*entry is for foundational purposes -- please ignore*)
- prefix: (string * bool) list, (*system prefix*)
- qualifier: (string * bool) list, (*user qualifier*)
- name: bstring, (*base name*)
- pos: Position.T}; (*source position*)
+ {limited: (bool * scope) option, (*entry is private (true) / restricted (false) to scope*)
+ concealed: bool, (*entry is for foundational purposes -- please ignore*)
+ prefix: (string * bool) list, (*system prefix*)
+ qualifier: (string * bool) list, (*user qualifier*)
+ name: bstring, (*base name*)
+ pos: Position.T}; (*source position*)
-fun make_binding (private, concealed, prefix, qualifier, name, pos) =
- Binding {private = private, concealed = concealed, prefix = prefix,
+fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
+ Binding {limited = limited, concealed = concealed, prefix = prefix,
qualifier = qualifier, name = name, pos = pos};
-fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
- make_binding (f (private, concealed, prefix, qualifier, name, pos));
+fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
+ make_binding (f (limited, concealed, prefix, qualifier, name, pos));
fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
@@ -83,8 +84,8 @@
fun pos_of (Binding {pos, ...}) = pos;
fun set_pos pos =
- map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
- (private, concealed, prefix, qualifier, name, pos));
+ map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
+ (limited, concealed, prefix, qualifier, name, pos));
fun name name = make (name, Position.none);
fun name_of (Binding {name, ...}) = name;
@@ -92,8 +93,8 @@
fun eq_name (b, b') = name_of b = name_of b';
fun map_name f =
- map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
- (private, concealed, prefix, qualifier, f name, pos));
+ map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+ (limited, concealed, prefix, qualifier, f name, pos));
val prefix_name = map_name o prefix;
val suffix_name = map_name o suffix;
@@ -106,13 +107,13 @@
fun qualify _ "" = I
| qualify mandatory qual =
- map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
- (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
+ map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+ (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
fun qualified mandatory name' =
- map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+ map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
- in (private, concealed, prefix, qualifier', name', pos) end);
+ in (limited, concealed, prefix, qualifier', name', pos) end);
fun qualified_name "" = empty
| qualified_name s =
@@ -125,8 +126,8 @@
fun prefix_of (Binding {prefix, ...}) = prefix;
fun map_prefix f =
- map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
- (private, concealed, f prefix, qualifier, name, pos));
+ map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+ (limited, concealed, f prefix, qualifier, name, pos));
fun prefix _ "" = I
| prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
@@ -134,17 +135,20 @@
(* visibility flags *)
-fun private scope =
+fun limited strict scope =
map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
- (SOME scope, concealed, prefix, qualifier, name, pos));
+ (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
-fun private_default private' =
- map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
- (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
+val private = limited true;
+val restricted = limited false;
+
+fun limited_default limited' =
+ map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+ (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
val concealed =
- map_binding (fn (private, _, prefix, qualifier, name, pos) =>
- (private, true, prefix, qualifier, name, pos));
+ map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
+ (limited, true, prefix, qualifier, name, pos));
(* print *)
@@ -177,13 +181,13 @@
fun name_spec scopes path binding =
let
- val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
+ val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
val _ = Long_Name.is_qualified name andalso error (bad binding);
- val accessible =
- (case private of
- NONE => true
- | SOME scope => member (op =) scopes scope);
+ val limitation =
+ (case limited of
+ NONE => NONE
+ | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
val spec1 =
maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
@@ -192,7 +196,7 @@
val _ =
exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
andalso error (bad binding);
- in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
+ in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
end;
--- a/src/Pure/General/name_space.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/General/name_space.ML Mon Apr 06 23:24:45 2015 +0200
@@ -35,8 +35,11 @@
val get_scopes: naming -> Binding.scope list
val get_scope: naming -> Binding.scope option
val new_scope: naming -> Binding.scope * naming
+ val limited: bool -> Position.T -> naming -> naming
val private_scope: Binding.scope -> naming -> naming
val private: Position.T -> naming -> naming
+ val restricted_scope: Binding.scope -> naming -> naming
+ val restricted: Position.T -> naming -> naming
val concealed: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
@@ -297,62 +300,73 @@
datatype naming = Naming of
{scopes: Binding.scope list,
- private: Binding.scope option,
+ limited: (bool * Binding.scope) option,
concealed: bool,
group: serial option,
theory_name: string,
path: (string * bool) list};
-fun make_naming (scopes, private, concealed, group, theory_name, path) =
- Naming {scopes = scopes, private = private, concealed = concealed,
+fun make_naming (scopes, limited, concealed, group, theory_name, path) =
+ Naming {scopes = scopes, limited = limited, concealed = concealed,
group = group, theory_name = theory_name, path = path};
-fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
- make_naming (f (scopes, private, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
+ make_naming (f (scopes, limited, concealed, group, theory_name, path));
-fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
- (scopes, private, concealed, group, theory_name, f path));
+(* scope and access limitation *)
fun get_scopes (Naming {scopes, ...}) = scopes;
val get_scope = try hd o get_scopes;
-fun put_scope scope =
- map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
- (scope :: scopes, private, concealed, group, theory_name, path));
-
fun new_scope naming =
let
val scope = Binding.new_scope ();
val naming' =
- naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
- (scope :: scopes, private, concealed, group, theory_name, path));
+ naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
+ (scope :: scopes, limited, concealed, group, theory_name, path));
in (scope, naming') end;
-fun private_scope scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
- (scopes, SOME scope, concealed, group, theory_name, path));
+fun limited_scope strict scope =
+ map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
+ (scopes, SOME (strict, scope), concealed, group, theory_name, path));
-fun private pos naming =
+fun limited strict pos naming =
(case get_scope naming of
- SOME scope => private_scope scope naming
- | NONE => error ("Missing local scope -- cannot declare private names" ^ Position.here pos));
+ SOME scope => limited_scope strict scope naming
+ | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
+
+val private_scope = limited_scope true;
+val private = limited true;
+
+val restricted_scope = limited_scope false;
+val restricted = limited false;
-val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
- (scopes, private, true, group, theory_name, path));
+val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
+ (scopes, limited, true, group, theory_name, path));
+
-fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
- (scopes, private, concealed, group, theory_name, path));
+(* additional structural info *)
+
+fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
+ (scopes, limited, concealed, group, theory_name, path));
fun get_group (Naming {group, ...}) = group;
-fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
- (scopes, private, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
+ (scopes, limited, concealed, group, theory_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
+
+(* name entry path *)
+
fun get_path (Naming {path, ...}) = path;
+fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
+ (scopes, limited, concealed, group, theory_name, f path));
+
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
val root_path = map_path (fn _ => []);
val parent_path = map_path (perhaps (try (#1 o split_last)));
@@ -365,14 +379,16 @@
val local_naming = global_naming |> add_path Long_Name.localN;
-(* visibility flags *)
+(* transform *)
-fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
- fold private_scope (the_list private') #>
+fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
+ (case limited' of
+ SOME (strict, scope) => limited_scope strict scope
+ | NONE => I) #>
concealed' ? concealed;
-fun transform_binding (Naming {private, concealed, ...}) =
- Binding.private_default private #>
+fun transform_binding (Naming {limited, concealed, ...}) =
+ Binding.limited_default limited #>
concealed ? Binding.concealed;
@@ -400,11 +416,12 @@
fun accesses naming binding =
(case name_spec naming binding of
- {accessible = false, ...} => ([], [])
- | {spec, ...} =>
+ {limitation = SOME true, ...} => ([], [])
+ | {limitation, spec, ...} =>
let
- val sfxs = mandatory_suffixes spec;
- val pfxs = mandatory_prefixes spec;
+ val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
+ val sfxs = restrict (mandatory_suffixes spec);
+ val pfxs = restrict (mandatory_prefixes spec);
in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
--- a/src/Pure/Isar/calculation.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Apr 06 23:24:45 2015 +0200
@@ -211,25 +211,25 @@
Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
val _ =
- Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
+ Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
(calc_args >> (Toplevel.proofs' o also_cmd));
val _ =
- Outer_Syntax.command @{command_spec "finally"}
+ Outer_Syntax.command @{command_keyword finally}
"combine calculation and current facts, exhibit result"
(calc_args >> (Toplevel.proofs' o finally_cmd));
val _ =
- Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
+ Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
(Scan.succeed (Toplevel.proof' moreover));
val _ =
- Outer_Syntax.command @{command_spec "ultimately"}
+ Outer_Syntax.command @{command_keyword ultimately}
"augment calculation by current facts, exhibit result"
(Scan.succeed (Toplevel.proof' ultimately));
val _ =
- Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
+ Outer_Syntax.command @{command_keyword 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_cmd.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Apr 06 23:24:45 2015 +0200
@@ -6,7 +6,7 @@
signature ISAR_CMD =
sig
- val global_setup: Input.source -> theory -> theory
+ val setup: Input.source -> theory -> theory
val local_setup: Input.source -> Proof.context -> Proof.context
val parse_ast_translation: Input.source -> theory -> theory
val parse_translation: Input.source -> theory -> theory
@@ -57,7 +57,7 @@
(* generic setup *)
-fun global_setup source =
+fun setup source =
ML_Lex.read_source false source
|> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
"Context.map_theory setup"
--- a/src/Pure/Isar/isar_syn.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Apr 06 23:24:45 2015 +0200
@@ -12,7 +12,7 @@
(* sorts *)
val _ =
- Outer_Syntax.local_theory @{command_spec "default_sort"}
+ Outer_Syntax.local_theory @{command_keyword default_sort}
"declare default sort for explicit type variables"
(Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
@@ -20,18 +20,18 @@
(* types *)
val _ =
- Outer_Syntax.local_theory @{command_spec "typedecl"} "type declaration"
+ Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
(Parse.type_args -- Parse.binding -- Parse.opt_mixfix
>> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
val _ =
- Outer_Syntax.local_theory @{command_spec "type_synonym"} "declare type abbreviation"
+ Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
(Parse.type_args -- Parse.binding --
(@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
>> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
val _ =
- Outer_Syntax.command @{command_spec "nonterminal"}
+ Outer_Syntax.command @{command_keyword nonterminal}
"declare syntactic type constructors (grammar nonterminal symbols)"
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
@@ -39,11 +39,11 @@
(* consts and syntax *)
val _ =
- Outer_Syntax.command @{command_spec "judgment"} "declare object-logic judgment"
+ Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
(Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
val _ =
- Outer_Syntax.command @{command_spec "consts"} "declare constants"
+ Outer_Syntax.command @{command_keyword consts} "declare constants"
(Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
val mode_spec =
@@ -54,12 +54,12 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
val _ =
- Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
+ Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
(opt_mode -- Scan.repeat1 Parse.const_decl
>> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
val _ =
- Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
+ Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
(opt_mode -- Scan.repeat1 Parse.const_decl
>> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
@@ -81,11 +81,11 @@
>> (fn (left, (arr, right)) => arr (left, right));
val _ =
- Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
+ Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
val _ =
- Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
+ Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
@@ -98,7 +98,7 @@
@{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
val _ =
- Outer_Syntax.command @{command_spec "defs"} "define constants"
+ Outer_Syntax.command @{command_keyword defs} "define constants"
(opt_unchecked_overloaded --
Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
>> (Toplevel.theory o Isar_Cmd.add_defs));
@@ -107,34 +107,34 @@
(* constant definitions and abbreviations *)
val _ =
- Outer_Syntax.local_theory' @{command_spec "definition"} "constant definition"
+ Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
(Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
val _ =
- Outer_Syntax.local_theory' @{command_spec "abbreviation"} "constant abbreviation"
+ Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
(opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
- Outer_Syntax.local_theory @{command_spec "type_notation"}
+ Outer_Syntax.local_theory @{command_keyword type_notation}
"add concrete syntax for type constructors"
(opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd true mode args));
val _ =
- Outer_Syntax.local_theory @{command_spec "no_type_notation"}
+ Outer_Syntax.local_theory @{command_keyword no_type_notation}
"delete concrete syntax for type constructors"
(opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd false mode args));
val _ =
- Outer_Syntax.local_theory @{command_spec "notation"}
+ Outer_Syntax.local_theory @{command_keyword notation}
"add concrete syntax for constants / fixed variables"
(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"}
+ Outer_Syntax.local_theory @{command_keyword no_notation}
"delete concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Specification.notation_cmd false mode args));
@@ -143,7 +143,7 @@
(* constant specifications *)
val _ =
- Outer_Syntax.command @{command_spec "axiomatization"} "axiomatic constant specification"
+ Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
(Scan.optional Parse.fixes [] --
Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
>> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
@@ -156,14 +156,14 @@
>> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
val _ =
- Outer_Syntax.local_theory' @{command_spec "theorems"} "define theorems"
+ Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems"
(theorems Thm.theoremK);
val _ =
- Outer_Syntax.local_theory' @{command_spec "lemmas"} "define lemmas" (theorems Thm.lemmaK);
+ Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" (theorems Thm.lemmaK);
val _ =
- Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
+ Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
(Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
@@ -173,8 +173,8 @@
local
-fun hide_names command_spec what hide parse prep =
- Outer_Syntax.command command_spec ("hide " ^ what ^ " from name space")
+fun hide_names command_keyword what hide parse prep =
+ Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
(Toplevel.theory (fn thy =>
let val ctxt = Proof_Context.init_global thy
@@ -183,19 +183,19 @@
in
val _ =
- hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
+ hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
Proof_Context.read_class;
val _ =
- hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
+ hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
val _ =
- hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
+ hide_names @{command_keyword hide_const} "constants" Sign.hide_const Parse.const
((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
val _ =
- hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
+ hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
(Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
end;
@@ -204,7 +204,7 @@
(* use ML text *)
val _ =
- Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
+ Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
(Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
let
val ([{lines, pos, ...}], thy') = files thy;
@@ -216,7 +216,7 @@
end)));
val _ =
- Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
+ Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
(Parse.ML_source >> (fn source =>
let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
Toplevel.theory
@@ -224,7 +224,7 @@
end));
val _ =
- Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
+ Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
(Parse.ML_source >> (fn source =>
let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
Toplevel.generic_theory
@@ -233,7 +233,7 @@
end));
val _ =
- Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
+ Outer_Syntax.command @{command_keyword ML} "ML text within theory or local theory"
(Parse.ML_source >> (fn source =>
Toplevel.generic_theory
(ML_Context.exec (fn () =>
@@ -241,7 +241,7 @@
Local_Theory.propagate_ml_env)));
val _ =
- Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
+ Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof"
(Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
(ML_Context.exec (fn () =>
@@ -249,45 +249,45 @@
Proof.propagate_ml_env)));
val _ =
- Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
+ Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text"
(Parse.ML_source >> Isar_Cmd.ml_diag true);
val _ =
- Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
+ Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)"
(Parse.ML_source >> Isar_Cmd.ml_diag false);
val _ =
- Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
- (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
+ Outer_Syntax.command @{command_keyword setup} "ML setup for global theory"
+ (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
val _ =
- Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup"
+ Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory"
(Parse.ML_source >> Isar_Cmd.local_setup);
val _ =
- Outer_Syntax.local_theory @{command_spec "attribute_setup"} "define attribute in ML"
+ Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
(Parse.position Parse.name --
Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
val _ =
- Outer_Syntax.local_theory @{command_spec "method_setup"} "define proof method in ML"
+ Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML"
(Parse.position Parse.name --
Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
val _ =
- Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
+ Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration"
(Parse.opt_keyword "pervasive" -- Parse.ML_source
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
val _ =
- Outer_Syntax.local_theory @{command_spec "syntax_declaration"} "generic ML syntax declaration"
+ Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration"
(Parse.opt_keyword "pervasive" -- Parse.ML_source
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
val _ =
- Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
+ Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
(Parse.position Parse.name --
(@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
@@ -297,27 +297,27 @@
(* translation functions *)
val _ =
- Outer_Syntax.command @{command_spec "parse_ast_translation"}
+ Outer_Syntax.command @{command_keyword parse_ast_translation}
"install parse ast translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
val _ =
- Outer_Syntax.command @{command_spec "parse_translation"}
+ Outer_Syntax.command @{command_keyword parse_translation}
"install parse translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
val _ =
- Outer_Syntax.command @{command_spec "print_translation"}
+ Outer_Syntax.command @{command_keyword print_translation}
"install print translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
val _ =
- Outer_Syntax.command @{command_spec "typed_print_translation"}
+ Outer_Syntax.command @{command_keyword typed_print_translation}
"install typed print translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
val _ =
- Outer_Syntax.command @{command_spec "print_ast_translation"}
+ Outer_Syntax.command @{command_keyword print_ast_translation}
"install print ast translation functions"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
@@ -325,7 +325,7 @@
(* oracles *)
val _ =
- Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
+ Outer_Syntax.command @{command_keyword oracle} "declare oracle"
(Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
(fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
@@ -333,22 +333,22 @@
(* bundled declarations *)
val _ =
- Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
+ Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
>> (uncurry Bundle.bundle_cmd));
val _ =
- Outer_Syntax.command @{command_spec "include"}
+ Outer_Syntax.command @{command_keyword include}
"include declarations from bundle in proof body"
(Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
val _ =
- Outer_Syntax.command @{command_spec "including"}
+ Outer_Syntax.command @{command_keyword including}
"include declarations from bundle in goal refinement"
(Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
val _ =
- Outer_Syntax.command @{command_spec "print_bundles"}
+ Outer_Syntax.command @{command_keyword print_bundles}
"print bundles of declarations"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
@@ -357,7 +357,7 @@
(* local theories *)
val _ =
- Outer_Syntax.command @{command_spec "context"} "begin local theory context"
+ Outer_Syntax.command @{command_keyword context} "begin local theory context"
((Parse.position Parse.xname >> (fn name =>
Toplevel.begin_local_theory true (Named_Target.begin name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
@@ -373,7 +373,7 @@
Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
val _ =
- Outer_Syntax.command @{command_spec "locale"} "define named specification context"
+ Outer_Syntax.command @{command_keyword locale} "define named specification context"
(Parse.binding --
Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
@@ -381,7 +381,7 @@
(Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
val _ =
- Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
+ Outer_Syntax.command @{command_keyword experiment} "open private specification context"
(Scan.repeat Parse_Spec.context_element --| Parse.begin
>> (fn elems =>
Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
@@ -392,7 +392,7 @@
(Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
val _ =
- Outer_Syntax.command @{command_spec "sublocale"}
+ Outer_Syntax.command @{command_keyword sublocale}
"prove sublocale relation between a locale and a locale expression"
((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
interpretation_args false >> (fn (loc, (expr, equations)) =>
@@ -401,13 +401,13 @@
Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
val _ =
- Outer_Syntax.command @{command_spec "interpretation"}
+ Outer_Syntax.command @{command_keyword interpretation}
"prove interpretation of locale expression in local theory"
(interpretation_args true >> (fn (expr, equations) =>
Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
val _ =
- Outer_Syntax.command @{command_spec "interpret"}
+ Outer_Syntax.command @{command_keyword interpret}
"prove interpretation of locale expression in proof context"
(interpretation_args true >> (fn (expr, equations) =>
Toplevel.proof' (Expression.interpret_cmd expr equations)));
@@ -421,23 +421,23 @@
Scan.repeat1 Parse_Spec.context_element >> pair [];
val _ =
- Outer_Syntax.command @{command_spec "class"} "define type class"
+ Outer_Syntax.command @{command_keyword class} "define type class"
(Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
Toplevel.begin_local_theory begin
(Class_Declaration.class_cmd name supclasses elems #> snd)));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
+ Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation"
(Parse.class >> Class_Declaration.subclass_cmd);
val _ =
- Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
+ Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity"
(Parse.multi_arity --| Parse.begin
>> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
val _ =
- Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
+ Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation"
((Parse.class --
((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
@@ -447,7 +447,7 @@
(* arbitrary overloading *)
val _ =
- Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
+ Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
(Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
>> Parse.triple1) --| Parse.begin
@@ -457,7 +457,7 @@
(* code generation *)
val _ =
- Outer_Syntax.command @{command_spec "code_datatype"}
+ Outer_Syntax.command @{command_keyword code_datatype}
"define set of code datatype constructors"
(Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
@@ -478,32 +478,32 @@
((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
kind NONE (K I) a includes elems concl)));
-val _ = theorem @{command_spec "theorem"} false Thm.theoremK;
-val _ = theorem @{command_spec "lemma"} false Thm.lemmaK;
-val _ = theorem @{command_spec "corollary"} false Thm.corollaryK;
-val _ = theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
-val _ = theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
-val _ = theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
+val _ = theorem @{command_keyword theorem} false Thm.theoremK;
+val _ = theorem @{command_keyword lemma} false Thm.lemmaK;
+val _ = theorem @{command_keyword corollary} false Thm.corollaryK;
+val _ = theorem @{command_keyword schematic_theorem} true Thm.theoremK;
+val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
+val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
+ Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
(Parse.begin >> K Proof.begin_notepad);
val _ =
- Outer_Syntax.command @{command_spec "have"} "state local goal"
+ Outer_Syntax.command @{command_keyword have} "state local goal"
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
val _ =
- Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
+ Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
val _ =
- Outer_Syntax.command @{command_spec "show"}
+ Outer_Syntax.command @{command_keyword show}
"state local goal, solving current obligation"
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
val _ =
- Outer_Syntax.command @{command_spec "thus"} "old-style alias of \"then show\""
+ Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
(Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
@@ -512,46 +512,46 @@
val facts = Parse.and_list1 Parse.xthms1;
val _ =
- Outer_Syntax.command @{command_spec "then"} "forward chaining"
+ Outer_Syntax.command @{command_keyword then} "forward chaining"
(Scan.succeed (Toplevel.proof Proof.chain));
val _ =
- Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
+ Outer_Syntax.command @{command_keyword from} "forward chaining from given facts"
(facts >> (Toplevel.proof o Proof.from_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
+ Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts"
(facts >> (Toplevel.proof o Proof.with_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_spec "note"} "define facts"
+ Outer_Syntax.command @{command_keyword note} "define facts"
(Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
val _ =
- Outer_Syntax.command @{command_spec "using"} "augment goal facts"
+ Outer_Syntax.command @{command_keyword using} "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
val _ =
- Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
+ Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
(facts >> (Toplevel.proof o Proof.unfolding_cmd));
(* proof context *)
val _ =
- Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
+ Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
(Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
val _ =
- Outer_Syntax.command @{command_spec "assume"} "assume propositions"
+ Outer_Syntax.command @{command_keyword assume} "assume propositions"
(Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
val _ =
- Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
+ Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
(Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
val _ =
- Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
+ Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
(Parse.and_list1
(Parse_Spec.opt_thm_name ":" --
((Parse.binding -- Parse.opt_mixfix) --
@@ -559,26 +559,26 @@
>> (Toplevel.proof o Proof.def_cmd));
val _ =
- Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
+ Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
(Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
>> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
- Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
+ Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
(Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
val _ =
- Outer_Syntax.command @{command_spec "let"} "bind text variables"
+ Outer_Syntax.command @{command_keyword let} "bind text variables"
(Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
>> (Toplevel.proof o Proof.let_bind_cmd));
val _ =
- Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
+ Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
>> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
val _ =
- Outer_Syntax.command @{command_spec "case"} "invoke local context"
+ Outer_Syntax.command @{command_keyword case} "invoke local context"
((@{keyword "("} |--
Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
--| @{keyword ")"}) ||
@@ -589,74 +589,74 @@
(* proof structure *)
val _ =
- Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
+ Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
(Scan.succeed (Toplevel.proof Proof.begin_block));
val _ =
- Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
+ Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
(Scan.succeed (Toplevel.proof Proof.end_block));
val _ =
- Outer_Syntax.command @{command_spec "next"} "enter next proof block"
+ Outer_Syntax.command @{command_keyword next} "enter next proof block"
(Scan.succeed (Toplevel.proof Proof.next_block));
(* end proof *)
val _ =
- Outer_Syntax.command @{command_spec "qed"} "conclude proof"
+ Outer_Syntax.command @{command_keyword qed} "conclude proof"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
Isar_Cmd.qed m)));
val _ =
- Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
+ Outer_Syntax.command @{command_keyword by} "terminal backward proof"
(Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
(Method.report m1;
Option.map Method.report m2;
Isar_Cmd.terminal_proof (m1, m2))));
val _ =
- Outer_Syntax.command @{command_spec ".."} "default proof"
+ Outer_Syntax.command @{command_keyword ".."} "default proof"
(Scan.succeed Isar_Cmd.default_proof);
val _ =
- Outer_Syntax.command @{command_spec "."} "immediate proof"
+ Outer_Syntax.command @{command_keyword "."} "immediate proof"
(Scan.succeed Isar_Cmd.immediate_proof);
val _ =
- Outer_Syntax.command @{command_spec "done"} "done proof"
+ Outer_Syntax.command @{command_keyword done} "done proof"
(Scan.succeed Isar_Cmd.done_proof);
val _ =
- Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
+ Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
(Scan.succeed Isar_Cmd.skip_proof);
val _ =
- Outer_Syntax.command @{command_spec "oops"} "forget proof"
+ Outer_Syntax.command @{command_keyword oops} "forget proof"
(Scan.succeed (Toplevel.forget_proof true));
(* proof steps *)
val _ =
- Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
+ Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
(Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
val _ =
- Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
+ Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
(Parse.nat >> (Toplevel.proof o Proof.prefer));
val _ =
- Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
+ Outer_Syntax.command @{command_keyword apply} "initial refinement step (unstructured)"
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
val _ =
- Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
+ Outer_Syntax.command @{command_keyword apply_end} "terminal refinement step (unstructured)"
(Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
val _ =
- Outer_Syntax.command @{command_spec "proof"} "backward proof step"
+ Outer_Syntax.command @{command_keyword proof} "backward proof step"
(Scan.option Method.parse >> (fn m =>
(Option.map Method.report m;
Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
@@ -669,7 +669,7 @@
Output.report [Markup.markup Markup.bad "Explicit backtracking"];
val _ =
- Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
+ Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
(Scan.succeed
(Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
Toplevel.skip_proof (fn h => (report_back (); h))));
@@ -682,194 +682,194 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val _ =
- Outer_Syntax.command @{command_spec "help"}
+ Outer_Syntax.command @{command_keyword help}
"retrieve outer syntax commands according to name patterns"
(Scan.repeat Parse.name >>
(fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
val _ =
- Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands"
+ Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
(Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_options"} "print configuration options"
+ Outer_Syntax.command @{command_keyword print_options} "print configuration options"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_context"}
+ Outer_Syntax.command @{command_keyword print_context}
"print context of local theory target"
(Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
val _ =
- Outer_Syntax.command @{command_spec "print_theory"}
+ Outer_Syntax.command @{command_keyword print_theory}
"print logical theory contents"
(Parse.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.command @{command_spec "print_syntax"}
+ Outer_Syntax.command @{command_keyword print_syntax}
"print inner syntax of context"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_defn_rules"}
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "print_abbrevs"}
+ Outer_Syntax.command @{command_keyword print_abbrevs}
"print constant abbreviations of context"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_theorems"}
+ Outer_Syntax.command @{command_keyword print_theorems}
"print theorems of local theory or proof context"
(Parse.opt_bang >> (fn b =>
Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
val _ =
- Outer_Syntax.command @{command_spec "print_locales"}
+ Outer_Syntax.command @{command_keyword print_locales}
"print locales of this theory"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_classes"}
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "print_locale"}
+ Outer_Syntax.command @{command_keyword print_locale}
"print locale of this theory"
(Parse.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.command @{command_spec "print_interps"}
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "print_dependencies"}
+ Outer_Syntax.command @{command_keyword print_dependencies}
"print dependencies of locale expression"
(Parse.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.command @{command_spec "print_attributes"}
+ Outer_Syntax.command @{command_keyword print_attributes}
"print attributes of this theory"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_simpset"}
+ Outer_Syntax.command @{command_keyword print_simpset}
"print context of Simplifier"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_rules"} "print intro/elim rules"
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "print_methods"} "print methods of this theory"
+ Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
(Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_antiquotations"}
+ Outer_Syntax.command @{command_keyword print_antiquotations}
"print document antiquotations"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_ML_antiquotations"}
+ Outer_Syntax.command @{command_keyword print_ML_antiquotations}
"print ML antiquotations"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "thy_deps"} "visualize theory dependencies"
+ Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
(Scan.succeed Isar_Cmd.thy_deps);
val _ =
- Outer_Syntax.command @{command_spec "locale_deps"} "visualize locale dependencies"
+ Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
(Scan.succeed Isar_Cmd.locale_deps);
val _ =
- Outer_Syntax.command @{command_spec "print_term_bindings"}
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "print_facts"} "print facts of proof context"
+ Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
(Parse.opt_bang >> (fn b => Toplevel.unknown_context o
Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_cases"} "print cases of proof context"
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "print_statement"}
+ Outer_Syntax.command @{command_keyword print_statement}
"print theorems as long statements"
(opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
val _ =
- Outer_Syntax.command @{command_spec "thm"} "print theorems"
+ Outer_Syntax.command @{command_keyword thm} "print theorems"
(opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
val _ =
- Outer_Syntax.command @{command_spec "prf"} "print proof terms of theorems"
+ Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
(opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
val _ =
- Outer_Syntax.command @{command_spec "full_prf"} "print full proof terms of theorems"
+ Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
(opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
val _ =
- Outer_Syntax.command @{command_spec "prop"} "read and print proposition"
+ Outer_Syntax.command @{command_keyword prop} "read and print proposition"
(opt_modes -- Parse.term >> Isar_Cmd.print_prop);
val _ =
- Outer_Syntax.command @{command_spec "term"} "read and print term"
+ Outer_Syntax.command @{command_keyword term} "read and print term"
(opt_modes -- Parse.term >> Isar_Cmd.print_term);
val _ =
- Outer_Syntax.command @{command_spec "typ"} "read and print type"
+ Outer_Syntax.command @{command_keyword typ} "read and print type"
(opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
>> Isar_Cmd.print_type);
val _ =
- Outer_Syntax.command @{command_spec "print_codesetup"} "print code generator setup"
+ Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
val _ =
- Outer_Syntax.command @{command_spec "print_state"}
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "welcome"} "print welcome message"
+ Outer_Syntax.command @{command_keyword welcome} "print welcome message"
(Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
val _ =
- Outer_Syntax.command @{command_spec "display_drafts"}
+ Outer_Syntax.command @{command_keyword 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)))));
@@ -881,24 +881,24 @@
val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
val _ =
- Outer_Syntax.command @{command_spec "realizers"}
+ Outer_Syntax.command @{command_keyword realizers}
"specify realizers for primitive axioms / theorems, together with correctness proof"
(Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
(fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
(map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
val _ =
- Outer_Syntax.command @{command_spec "realizability"}
+ Outer_Syntax.command @{command_keyword realizability}
"add equations characterizing realizability"
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
val _ =
- Outer_Syntax.command @{command_spec "extract_type"}
+ Outer_Syntax.command @{command_keyword extract_type}
"add equations characterizing type of extracted program"
(Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
val _ =
- Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
+ Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
(Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
@@ -907,10 +907,9 @@
(** end **)
val _ =
- Outer_Syntax.command @{command_spec "end"} "end context"
+ Outer_Syntax.command @{command_keyword end} "end context"
(Scan.succeed
(Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
Toplevel.end_proof (K Proof.end_notepad)));
end;
-
--- a/src/Pure/Isar/keyword.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Apr 06 23:24:45 2015 +0200
@@ -37,10 +37,11 @@
val no_command_keywords: keywords -> keywords
val empty_keywords: keywords
val merge_keywords: keywords * keywords -> keywords
- val add_keywords: (string * spec option) list -> keywords -> keywords
+ val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
val is_keyword: keywords -> string -> bool
val is_command: keywords -> string -> bool
val is_literal: keywords -> string -> bool
+ val command_markup: keywords -> string -> Markup.T option
val command_kind: keywords -> string -> string option
val command_files: keywords -> string -> Path.T -> Path.T list
val command_tags: keywords -> string -> string list
@@ -105,19 +106,21 @@
(* specifications *)
-type T =
- {kind: string,
+type spec = (string * string list) * string list;
+
+type entry =
+ {pos: Position.T,
+ id: serial,
+ kind: string,
files: string list, (*extensions of embedded files*)
tags: string list};
-type spec = (string * string list) * string list;
-
-fun check_spec ((kind, files), tags) : T =
+fun check_spec pos ((kind, files), tags) : entry =
if not (member (op =) kinds kind) then
error ("Unknown outer syntax keyword kind " ^ quote kind)
else if not (null files) andalso kind <> thy_load then
error ("Illegal specification of files for " ^ quote kind)
- else {kind = kind, files = files, tags = tags};
+ else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
@@ -128,7 +131,7 @@
datatype keywords = Keywords of
{minor: Scan.lexicon,
major: Scan.lexicon,
- commands: T Symtab.table};
+ commands: entry Symtab.table};
fun minor_keywords (Keywords {minor, ...}) = minor;
fun major_keywords (Keywords {major, ...}) = major;
@@ -157,7 +160,7 @@
Symtab.merge (K true) (commands1, commands2));
val add_keywords =
- fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) =>
+ fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
(case opt_spec of
NONE =>
let
@@ -165,9 +168,9 @@
in (minor', major, commands) end
| SOME spec =>
let
- val kind = check_spec spec;
+ val entry = check_spec pos spec;
val major' = Scan.extend_lexicon (Symbol.explode name) major;
- val commands' = Symtab.update (name, kind) commands;
+ val commands' = Symtab.update (name, entry) commands;
in (minor, major', commands') end)));
@@ -178,10 +181,16 @@
fun is_literal keywords = is_keyword keywords orf is_command keywords;
-(* command kind *)
+(* command keywords *)
fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
+fun command_markup keywords name =
+ lookup_command keywords name
+ |> Option.map (fn {pos, id, ...} =>
+ Markup.properties (Position.entity_properties_of false id pos)
+ (Markup.entity Markup.command_keywordN name));
+
fun command_kind keywords = Option.map #kind o lookup_command keywords;
fun command_files keywords name path =
--- a/src/Pure/Isar/outer_syntax.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Apr 06 23:24:45 2015 +0200
@@ -8,16 +8,16 @@
sig
val help: theory -> string list -> unit
val print_commands: theory -> unit
- type command_spec = string * Position.T
- val command: command_spec -> string ->
+ type command_keyword = string * Position.T
+ val command: command_keyword -> string ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val local_theory': command_spec -> string ->
+ val local_theory': command_keyword -> string ->
(bool -> local_theory -> local_theory) parser -> unit
- val local_theory: command_spec -> string ->
+ val local_theory: command_keyword -> string ->
(local_theory -> local_theory) parser -> unit
- val local_theory_to_proof': command_spec -> string ->
+ val local_theory_to_proof': command_keyword -> string ->
(bool -> local_theory -> Proof.state) parser -> unit
- val local_theory_to_proof: command_spec -> string ->
+ val local_theory_to_proof: command_keyword -> string ->
(local_theory -> Proof.state) parser -> unit
val parse: theory -> Position.T -> string -> Toplevel.transition list
val parse_tokens: theory -> Token.T list -> Toplevel.transition list
@@ -44,7 +44,8 @@
datatype command_parser =
Parser of (Toplevel.transition -> Toplevel.transition) parser |
- Private_Parser of Position.T option -> (Toplevel.transition -> Toplevel.transition) parser;
+ Limited_Parser of
+ (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
datatype command = Command of
{comment: string,
@@ -134,18 +135,19 @@
(* implicit theory setup *)
-type command_spec = string * Position.T;
+type command_keyword = string * Position.T;
fun raw_command (name, pos) comment command_parser =
- Theory.setup (add_command name (new_command comment command_parser pos));
+ let val setup = add_command name (new_command comment command_parser pos)
+ in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
fun command (name, pos) comment parse =
raw_command (name, pos) comment (Parser parse);
-fun local_theory_command trans command_spec comment parse =
- raw_command command_spec comment
- (Private_Parser (fn private =>
- Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
+fun local_theory_command trans command_keyword comment parse =
+ raw_command command_keyword comment
+ (Limited_Parser (fn limited =>
+ Parse.opt_target -- parse >> (fn (target, f) => trans limited target f)));
val local_theory' = local_theory_command Toplevel.local_theory';
val local_theory = local_theory_command Toplevel.local_theory;
@@ -160,8 +162,11 @@
local
+val before_command =
+ Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
+
fun parse_command thy =
- Scan.ahead (Parse.opt_private |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
+ Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
let
val command_tags = Parse.command_ -- Parse.tags;
val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
@@ -169,9 +174,9 @@
(case lookup_commands thy name of
SOME (Command {command_parser = Parser parse, ...}) =>
Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
- | SOME (Command {command_parser = Private_Parser parse, ...}) =>
- Parse.opt_private :|-- (fn private =>
- Parse.!!! (command_tags |-- parse private)) >> (fn f => f tr0)
+ | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
+ before_command :|-- (fn limited =>
+ Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
| NONE =>
Scan.succeed
(tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
@@ -224,9 +229,9 @@
fun parse tok (result, content, improper) =
if Token.is_improper tok then (result, content, tok :: improper)
- else if Token.is_private tok orelse
+ else if Token.is_command_modifier tok orelse
Token.is_command tok andalso
- (not (exists Token.is_private content) orelse exists Token.is_command content)
+ (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
then (flush (result, content, improper), [tok], [])
else (result, tok :: (improper @ content), []);
--- a/src/Pure/Isar/outer_syntax.scala Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Mon Apr 06 23:24:45 2015 +0200
@@ -219,8 +219,8 @@
for (tok <- toks) {
if (tok.is_improper) improper += tok
- else if (tok.is_private ||
- tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
+ else if (tok.is_command_modifier ||
+ tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
{ flush(); content += tok }
else { content ++= improper; improper.clear; content += tok }
}
--- a/src/Pure/Isar/parse.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/parse.ML Mon Apr 06 23:24:45 2015 +0200
@@ -104,7 +104,7 @@
val propp: (string * string list) parser
val termp: (string * string list) parser
val private: Position.T parser
- val opt_private: Position.T option parser
+ val restricted: Position.T parser
val target: (xstring * Position.T) parser
val opt_target: (xstring * Position.T) option parser
val args: Token.T list parser
@@ -401,7 +401,7 @@
(* target information *)
val private = position ($$$ "private") >> #2;
-val opt_private = Scan.option private;
+val restricted = position ($$$ "restricted") >> #2;
val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
val opt_target = Scan.option target;
--- a/src/Pure/Isar/proof_context.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Apr 06 23:24:45 2015 +0200
@@ -38,6 +38,8 @@
val new_scope: Proof.context -> Binding.scope * Proof.context
val private_scope: Binding.scope -> Proof.context -> Proof.context
val private: Position.T -> Proof.context -> Proof.context
+ val restricted_scope: Binding.scope -> Proof.context -> Proof.context
+ val restricted: Position.T -> Proof.context -> Proof.context
val concealed: Proof.context -> Proof.context
val class_space: Proof.context -> Name_Space.T
val type_space: Proof.context -> Name_Space.T
@@ -319,6 +321,9 @@
val private_scope = map_naming o Name_Space.private_scope;
val private = map_naming o Name_Space.private;
+val restricted_scope = map_naming o Name_Space.restricted_scope;
+val restricted = map_naming o Name_Space.restricted;
+
val concealed = map_naming Name_Space.concealed;
--- a/src/Pure/Isar/token.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/token.ML Mon Apr 06 23:24:45 2015 +0200
@@ -46,7 +46,7 @@
val is_command: T -> bool
val is_name: T -> bool
val keyword_with: (string -> bool) -> T -> bool
- val is_private: T -> bool
+ val is_command_modifier: T -> bool
val ident_with: (string -> bool) -> T -> bool
val is_proper: T -> bool
val is_improper: T -> bool
@@ -247,7 +247,7 @@
fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
| keyword_with _ _ = false;
-val is_private = keyword_with (fn x => x = "private");
+val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
fun ident_with pred (Token (_, (Ident, x), _)) = pred x
| ident_with _ _ = false;
--- a/src/Pure/Isar/token.scala Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/token.scala Mon Apr 06 23:24:45 2015 +0200
@@ -259,7 +259,8 @@
def is_begin: Boolean = is_keyword && source == "begin"
def is_end: Boolean = is_command && source == "end"
- def is_private: Boolean = is_keyword && source == "private"
+ def is_command_modifier: Boolean =
+ is_keyword && (source == "private" || source == "restricted")
def is_begin_block: Boolean = is_command && source == "{"
def is_end_block: Boolean = is_command && source == "}"
--- a/src/Pure/Isar/toplevel.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Apr 06 23:24:45 2015 +0200
@@ -51,15 +51,15 @@
val end_local_theory: transition -> transition
val open_target: (generic_theory -> local_theory) -> transition -> transition
val close_target: transition -> transition
- val local_theory': Position.T option -> (xstring * Position.T) option ->
+ val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
(bool -> local_theory -> local_theory) -> transition -> transition
- val local_theory: Position.T option -> (xstring * Position.T) option ->
+ val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
(local_theory -> local_theory) -> transition -> transition
val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
transition -> transition
- val local_theory_to_proof': Position.T option -> (xstring * Position.T) option ->
+ val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
(bool -> local_theory -> Proof.state) -> transition -> transition
- val local_theory_to_proof: Position.T option -> (xstring * Position.T) option ->
+ val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option ->
(local_theory -> Proof.state) -> transition -> transition
val theory_to_proof: (theory -> Proof.state) -> transition -> transition
val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
@@ -412,12 +412,15 @@
| NONE => raise UNDEF)
| _ => raise UNDEF));
-fun local_theory' private target f = present_transaction (fn int =>
+val limited_context =
+ fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
+
+fun local_theory' limited target f = present_transaction (fn int =>
(fn Theory (gthy, _) =>
let
val (finish, lthy) = Named_Target.switch target gthy;
val lthy' = lthy
- |> fold Proof_Context.private (the_list private)
+ |> limited_context limited
|> Local_Theory.new_group
|> f int
|> Local_Theory.reset_group;
@@ -425,7 +428,7 @@
| _ => raise UNDEF))
(K ());
-fun local_theory private target f = local_theory' private target (K f);
+fun local_theory limited target f = local_theory' limited target (K f);
fun present_local_theory target = present_transaction (fn int =>
(fn Theory (gthy, _) =>
@@ -470,18 +473,18 @@
in
-fun local_theory_to_proof' private target f = begin_proof
+fun local_theory_to_proof' limited target f = begin_proof
(fn int => fn gthy =>
let
val (finish, lthy) = Named_Target.switch target gthy;
val prf = lthy
- |> fold Proof_Context.private (the_list private)
+ |> limited_context limited
|> Local_Theory.new_group
|> f int;
in (finish o Local_Theory.reset_group, prf) end);
-fun local_theory_to_proof private target f =
- local_theory_to_proof' private target (K f);
+fun local_theory_to_proof limited target f =
+ local_theory_to_proof' limited target (K f);
fun theory_to_proof f = begin_proof
(fn _ => fn gthy =>
--- a/src/Pure/ML/ml_antiquotations.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Apr 06 23:24:45 2015 +0200
@@ -253,11 +253,12 @@
if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
"Parse.$$$ " ^ ML_Syntax.print_string name
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
- ML_Antiquotation.value @{binding command_spec}
- (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
- if Keyword.is_command (Thy_Header.get_keywords thy) name then
- ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
- else error ("Bad outer syntax command " ^ quote name ^ Position.here pos))));
+ ML_Antiquotation.value @{binding command_keyword}
+ (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
+ (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
+ SOME markup =>
+ (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
+ ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
+ | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
end;
-
--- a/src/Pure/PIDE/document.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/PIDE/document.ML Mon Apr 06 23:24:45 2015 +0200
@@ -125,8 +125,8 @@
NONE => I
| SOME id => Protocol_Message.command_positions_yxml id)
|> error;
- val {name = (name, _), imports, keywords} = header;
- val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
+ val {name = (name, _), imports, ...} = header;
+ val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
fun get_perspective (Node {perspective, ...}) = perspective;
--- a/src/Pure/PIDE/markup.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/PIDE/markup.ML Mon Apr 06 23:24:45 2015 +0200
@@ -115,6 +115,7 @@
val paragraphN: string val paragraph: T
val text_foldN: string val text_fold: T
val inputN: string val input: bool -> Properties.T -> T
+ val command_keywordN: string val command_keyword: T
val commandN: string val command: T
val stringN: string val string: T
val alt_stringN: string val alt_string: T
@@ -464,6 +465,7 @@
(* outer syntax *)
+val (command_keywordN, command_keyword) = markup_elem "command_keyword";
val (commandN, command) = markup_elem "command";
val (keyword1N, keyword1) = markup_elem "keyword1";
val (keyword2N, keyword2) = markup_elem "keyword2";
--- a/src/Pure/PIDE/protocol.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Apr 06 23:24:45 2015 +0200
@@ -81,7 +81,8 @@
(option (pair (pair string (list string)) (list string)))))
(list YXML.string_of_body)))) a;
val imports' = map (rpair Position.none) imports;
- val header = Thy_Header.make (name, Position.none) imports' keywords;
+ val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+ val header = Thy_Header.make (name, Position.none) imports' keywords';
in Document.Deps {master = master, header = header, errors = errors} end,
fn (a :: b, c) =>
Document.Perspective (bool_atom a, map int_atom b,
--- a/src/Pure/Pure.thy Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Pure.thy Mon Apr 06 23:24:45 2015 +0200
@@ -11,8 +11,8 @@
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
- "overloaded" "pervasive" "private" "shows" "structure" "unchecked"
- "where" "|"
+ "overloaded" "pervasive" "private" "restricted" "shows"
+ "structure" "unchecked" "where" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
and "default_sort" :: thy_decl == ""
--- a/src/Pure/Thy/thy_header.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Apr 06 23:24:45 2015 +0200
@@ -6,7 +6,7 @@
signature THY_HEADER =
sig
- type keywords = (string * Keyword.spec option) list
+ type keywords = ((string * Position.T) * Keyword.spec option) list
type header =
{name: string * Position.T,
imports: (string * Position.T) list,
@@ -29,7 +29,7 @@
(* header *)
-type keywords = (string * Keyword.spec option) list;
+type keywords = ((string * Position.T) * Keyword.spec option) list;
type header =
{name: string * Position.T,
@@ -59,26 +59,26 @@
val bootstrap_keywords =
Keyword.empty_keywords
|> Keyword.add_keywords
- [("%", NONE),
- ("(", NONE),
- (")", NONE),
- (",", NONE),
- ("::", NONE),
- ("==", NONE),
- ("and", NONE),
- (beginN, NONE),
- (importsN, NONE),
- (keywordsN, NONE),
- (headerN, SOME ((Keyword.document_heading, []), [])),
- (chapterN, SOME ((Keyword.document_heading, []), [])),
- (sectionN, SOME ((Keyword.document_heading, []), [])),
- (subsectionN, SOME ((Keyword.document_heading, []), [])),
- (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
- (textN, SOME ((Keyword.document_body, []), [])),
- (txtN, SOME ((Keyword.document_body, []), [])),
- (text_rawN, SOME ((Keyword.document_raw, []), [])),
- (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
- ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
+ [(("%", @{here}), NONE),
+ (("(", @{here}), NONE),
+ ((")", @{here}), NONE),
+ ((",", @{here}), NONE),
+ (("::", @{here}), NONE),
+ (("==", @{here}), NONE),
+ (("and", @{here}), NONE),
+ ((beginN, @{here}), NONE),
+ ((importsN, @{here}), NONE),
+ ((keywordsN, @{here}), NONE),
+ ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
+ ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
+ ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
+ ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
+ (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
(* theory data *)
@@ -119,7 +119,7 @@
Parse.group (fn () => "outer syntax keyword completion") Parse.name;
val keyword_decl =
- Scan.repeat1 Parse.string --
+ Scan.repeat1 (Parse.position Parse.string) --
Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
>> (fn ((names, spec), _) => map (rpair spec) names);
--- a/src/Pure/Thy/thy_output.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Apr 06 23:24:45 2015 +0200
@@ -384,10 +384,10 @@
in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
val command = Scan.peek (fn d =>
- Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
+ Scan.optional (Scan.one Token.is_command_modifier -- improper >> op ::) [] --
Scan.one Token.is_command -- Scan.repeat tag
- >> (fn ((private, cmd), tags) =>
- map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
+ >> (fn ((cmd_mod, cmd), tags) =>
+ map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
[(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
(Basic_Token cmd, (Latex.markup_false, d)))]));
--- a/src/Pure/Tools/class_deps.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML Mon Apr 06 23:24:45 2015 +0200
@@ -46,7 +46,7 @@
|| (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
val _ =
- Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
+ Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) =>
(Toplevel.unknown_theory o
Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
--- a/src/Pure/Tools/find_consts.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML Mon Apr 06 23:24:45 2015 +0200
@@ -140,7 +140,7 @@
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
-val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
in
@@ -151,7 +151,7 @@
|> #1;
val _ =
- Outer_Syntax.command @{command_spec "find_consts"}
+ Outer_Syntax.command @{command_keyword find_consts}
"find constants by name / type patterns"
(query >> (fn spec =>
Toplevel.keep (fn st =>
--- a/src/Pure/Tools/find_theorems.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Apr 06 23:24:45 2015 +0200
@@ -524,7 +524,7 @@
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
-val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
in
@@ -535,7 +535,7 @@
|> #1;
val _ =
- Outer_Syntax.command @{command_spec "find_theorems"}
+ Outer_Syntax.command @{command_keyword find_theorems}
"find theorems meeting specified criteria"
(options -- query >> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.keep (fn st =>
--- a/src/Pure/Tools/named_theorems.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML Mon Apr 06 23:24:45 2015 +0200
@@ -89,7 +89,7 @@
in (name, lthy') end;
val _ =
- Outer_Syntax.local_theory @{command_spec "named_theorems"}
+ Outer_Syntax.local_theory @{command_keyword named_theorems}
"declare named collection of theorems"
(Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
fold (fn (b, descr) => snd o declare b descr));
--- a/src/Pure/Tools/rail.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Tools/rail.ML Mon Apr 06 23:24:45 2015 +0200
@@ -363,8 +363,7 @@
in
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding rail}
- (Scan.lift (Parse.input (Parse.string || Parse.cartouche)))
+ (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
(fn {state, context, ...} => output_rules state o read context));
end;
--- a/src/Pure/Tools/thm_deps.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML Mon Apr 06 23:24:45 2015 +0200
@@ -44,7 +44,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
+ Outer_Syntax.command @{command_keyword 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))));
@@ -101,7 +101,7 @@
in rev thms' end;
val _ =
- Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
+ Outer_Syntax.command @{command_keyword 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/Pure/sign.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/sign.ML Mon Apr 06 23:24:45 2015 +0200
@@ -525,6 +525,8 @@
val private_scope = map_naming o Name_Space.private_scope;
val private = map_naming o Name_Space.private;
+val restricted_scope = map_naming o Name_Space.restricted_scope;
+val restricted = map_naming o Name_Space.restricted;
val concealed = map_naming Name_Space.concealed;
--- a/src/Pure/theory.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Pure/theory.ML Mon Apr 06 23:24:45 2015 +0200
@@ -14,6 +14,7 @@
val merge: theory * theory -> theory
val merge_list: theory list -> theory
val setup: (theory -> theory) -> unit
+ val local_setup: (Proof.context -> Proof.context) -> unit
val get_markup: theory -> Markup.T
val axiom_table: theory -> term Name_Space.table
val axiom_space: theory -> Name_Space.T
@@ -51,6 +52,7 @@
| merge_list (thy :: thys) = Library.foldl merge (thy, thys);
fun setup f = Context.>> (Context.map_theory f);
+fun local_setup f = Context.>> (Context.map_proof f);
--- a/src/Sequents/prover.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Sequents/prover.ML Mon Apr 06 23:24:45 2015 +0200
@@ -68,7 +68,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_pack"} "print pack of classical rules"
+ Outer_Syntax.command @{command_keyword print_pack} "print pack of classical rules"
(Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of)));
--- a/src/Tools/Code/code_haskell.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Apr 06 23:24:45 2015 +0200
@@ -516,7 +516,7 @@
#> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr);
val _ =
- Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
+ Outer_Syntax.command @{command_keyword code_monad} "define code syntax for monads"
(Parse.term -- Parse.name >> (fn (raw_bind, target) =>
Toplevel.theory (add_monad target raw_bind)));
--- a/src/Tools/Code/code_preproc.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Apr 06 23:24:45 2015 +0200
@@ -588,7 +588,7 @@
end);
val _ =
- Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
+ Outer_Syntax.command @{command_keyword 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_runtime.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/Code/code_runtime.ML Mon Apr 06 23:24:45 2015 +0200
@@ -475,7 +475,7 @@
in
val _ =
- Outer_Syntax.command @{command_spec "code_reflect"}
+ Outer_Syntax.command @{command_keyword code_reflect}
"enrich runtime environment with generated code"
(Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
--- a/src/Tools/Code/code_target.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/Code/code_target.ML Mon Apr 06 23:24:45 2015 +0200
@@ -638,25 +638,25 @@
:|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
val _ =
- Outer_Syntax.command @{command_spec "code_reserved"}
+ Outer_Syntax.command @{command_keyword code_reserved}
"declare words as reserved for target language"
(Parse.name -- Scan.repeat1 Parse.name
>> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
val _ =
- Outer_Syntax.command @{command_spec "code_identifier"} "declare mandatory names for code symbols"
+ Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
(parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
>> (Toplevel.theory o fold set_identifiers_cmd));
val _ =
- Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
+ Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
(parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
(Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
>> (Toplevel.theory o fold set_printings_cmd));
val _ =
- Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
+ Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
(Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
end; (*struct*)
--- a/src/Tools/Code/code_thingol.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Apr 06 23:24:45 2015 +0200
@@ -957,14 +957,14 @@
in
val _ =
- Outer_Syntax.command @{command_spec "code_thms"}
+ Outer_Syntax.command @{command_keyword 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.command @{command_spec "code_deps"}
+ Outer_Syntax.command @{command_keyword code_deps}
"visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.unknown_context o
--- a/src/Tools/adhoc_overloading.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/adhoc_overloading.ML Mon Apr 06 23:24:45 2015 +0200
@@ -233,12 +233,12 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
+ Outer_Syntax.local_theory @{command_keyword adhoc_overloading}
"add adhoc overloading for constants / fixed variables"
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
val _ =
- Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
+ Outer_Syntax.local_theory @{command_keyword no_adhoc_overloading}
"delete adhoc overloading for constants / fixed variables"
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
--- a/src/Tools/induct.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/induct.ML Mon Apr 06 23:24:45 2015 +0200
@@ -88,7 +88,7 @@
(Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic) ->
- theory -> theory
+ local_theory -> local_theory
end;
functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
@@ -162,7 +162,7 @@
val rearrange_eqs_simproc =
Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
- (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t));
+ (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t));
(* rotate k premises to the left by j, skipping over first j premises *)
@@ -257,7 +257,7 @@
end;
val _ =
- Outer_Syntax.command @{command_spec "print_induct_rules"}
+ Outer_Syntax.command @{command_keyword print_induct_rules}
"print induction and cases rules"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_rules o Toplevel.context_of)));
@@ -363,14 +363,14 @@
in
val _ =
- Theory.setup
- (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
+ Theory.local_setup
+ (Attrib.local_setup @{binding cases} (attrib cases_type cases_pred cases_del)
"declaration of cases rule" #>
- Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
+ Attrib.local_setup @{binding induct} (attrib induct_type induct_pred induct_del)
"declaration of induction rule" #>
- Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
+ Attrib.local_setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
"declaration of coinduction rule" #>
- Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
+ Attrib.local_setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
"declaration of rules for simplifying induction or cases rules");
end;
@@ -515,7 +515,7 @@
(** induct method **)
-val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
+val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction};
(* atomize *)
@@ -549,7 +549,7 @@
rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN'
Goal.conjunction_tac THEN_ALL_NEW
- (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt);
+ (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt);
(* prepare rule *)
@@ -737,10 +737,10 @@
SUBGOAL_CASES (fn (_, i, st) =>
let
val thy = Proof_Context.theory_of ctxt;
-
+
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
-
+
fun inst_rule (concls, r) =
(if null insts then `Rule_Cases.get r
else (align_left "Rule has fewer conclusions than arguments given"
@@ -749,7 +749,7 @@
|> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
|> mod_cases thy
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
-
+
val ruleq =
(case opt_rule of
SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
@@ -759,7 +759,7 @@
|> map_filter (Rule_Cases.mutual_rule ctxt)
|> tap (trace_rules ctxt inductN o map #2)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-
+
fun rule_cases ctxt rule cases =
let
val rule' = Rule_Cases.internalize_params rule;
@@ -910,18 +910,8 @@
in
-val _ =
- Theory.setup
- (Method.setup @{binding cases}
- (Scan.lift (Args.mode no_simpN) --
- (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
- (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
- METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
- (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
- "case analysis on types or predicates/sets");
-
fun gen_induct_setup binding tac =
- Method.setup binding
+ Method.local_setup binding
(Scan.lift (Args.mode no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) >>
@@ -929,11 +919,17 @@
Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
"induction on types or predicates/sets";
-val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
-
val _ =
- Theory.setup
- (Method.setup @{binding coinduct}
+ Theory.local_setup
+ (Method.local_setup @{binding cases}
+ (Scan.lift (Args.mode no_simpN) --
+ (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+ (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
+ METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
+ (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
+ "case analysis on types or predicates/sets" #>
+ gen_induct_setup @{binding induct} induct_tac #>
+ Method.local_setup @{binding coinduct}
(Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
(fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
--- a/src/Tools/induction.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/induction.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1,6 +1,14 @@
+(* Title: Tools/induction.ML
+ Author: Tobias Nipkow, TU Muenchen
+
+Alternative proof method "induction" that gives induction hypotheses the
+name "IH".
+*)
+
signature INDUCTION =
sig
- val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ val induction_tac: Proof.context -> bool ->
+ (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
end
@@ -11,13 +19,13 @@
val ind_hypsN = "IH";
fun preds_of t =
- (case strip_comb t of
+ (case strip_comb t of
(p as Var _, _) => [p]
| (p as Free _, _) => [p]
- | (_, ts) => flat(map preds_of ts))
+ | (_, ts) => maps preds_of ts);
fun name_hyps (arg as ((cases, consumes), th)) =
- if not(forall (null o #2 o #1) cases) then arg
+ if not (forall (null o #2 o #1) cases) then arg
else
let
val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
@@ -25,18 +33,18 @@
val ps = preds_of concl;
fun hname_of t =
- if exists_subterm (member (op =) ps) t
- then ind_hypsN else Rule_Cases.case_hypsN
+ if exists_subterm (member (op aconv) ps) t
+ then ind_hypsN else Rule_Cases.case_hypsN;
- val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
- val n = Int.min (length hnamess, length cases)
- val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
- (take n cases ~~ take n hnamess)
- in ((cases',consumes),th) end
+ val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
+ val n = Int.min (length hnamess, length cases);
+ val cases' =
+ map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
+ (take n cases ~~ take n hnamess);
+ in ((cases', consumes), th) end;
-val induction_tac = Induct.gen_induct_tac (K name_hyps)
+val induction_tac = Induct.gen_induct_tac (K name_hyps);
-val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
+val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
end
-
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Apr 06 23:24:45 2015 +0200
@@ -39,10 +39,18 @@
protected var _end = int_to_pos(range.stop)
override def getIcon: Icon = null
override def getShortString: String =
- "<html><span style=\"" + css + "\">" +
- (if (keyword != "" && _name.startsWith(keyword))
- "<b>" + HTML.encode(keyword) + "</b>" + HTML.encode(_name.substring(keyword.length))
- else HTML.encode(_name)) + "</span></html>"
+ {
+ val n = keyword.length
+ val s =
+ _name.indexOf(keyword) match {
+ case i if i >= 0 && n > 0 =>
+ HTML.encode(_name.substring(0, i)) +
+ "<b>" + HTML.encode(keyword) + "</b>" +
+ HTML.encode(_name.substring(i + n))
+ case _ => HTML.encode(_name)
+ }
+ "<html><span style=\"" + css + "\">" + s + "</span></html>"
+ }
override def getLongString: String = _name
override def getName: String = _name
override def setName(name: String) = _name = name
--- a/src/Tools/jEdit/src/token_markup.scala Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Apr 06 23:24:45 2015 +0200
@@ -274,11 +274,11 @@
{
def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
token_reverse_iterator(syntax, buffer, i).
- find(info => info.info.is_private || info.info.is_command)
+ find(info => info.info.is_command_modifier || info.info.is_command)
def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
token_iterator(syntax, buffer, i).
- find(info => info.info.is_private || info.info.is_command)
+ find(info => info.info.is_command_modifier || info.info.is_command)
if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
val start_info =
@@ -288,15 +288,15 @@
case Some(Text.Info(range1, tok1)) if tok1.is_command =>
val info2 = maybe_command_start(range1.start - 1)
info2 match {
- case Some(Text.Info(_, tok2)) if tok2.is_private => info2
+ case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
case _ => info1
}
case _ => info1
}
}
- val (start_is_private, start, start_next) =
+ val (start_is_command_modifier, start, start_next) =
start_info match {
- case Some(Text.Info(range, tok)) => (tok.is_private, range.start, range.stop)
+ case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
case None => (false, 0, 0)
}
@@ -304,7 +304,7 @@
{
val info1 = maybe_command_stop(start_next)
info1 match {
- case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_private =>
+ case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
maybe_command_stop(range1.stop)
case _ => info1
}
--- a/src/Tools/permanent_interpretation.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/permanent_interpretation.ML Mon Apr 06 23:24:45 2015 +0200
@@ -95,7 +95,7 @@
end;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
"prove interpretation of locale expression into named theory"
(Parse.!!! (Parse_Spec.locale_expression true) --
Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
--- a/src/Tools/quickcheck.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/quickcheck.ML Mon Apr 06 23:24:45 2015 +0200
@@ -527,11 +527,11 @@
@{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
val _ =
- Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
+ Outer_Syntax.command @{command_keyword quickcheck_params} "set parameters for random testing"
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
val _ =
- Outer_Syntax.command @{command_spec "quickcheck"}
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/solve_direct.ML Mon Apr 06 23:24:45 2015 +0200
@@ -92,7 +92,7 @@
val solve_direct = do_solve_direct Normal
val _ =
- Outer_Syntax.command @{command_spec "solve_direct"}
+ Outer_Syntax.command @{command_keyword 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 Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/subtyping.ML Mon Apr 06 23:24:45 2015 +0200
@@ -1115,7 +1115,7 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.command @{command_spec "print_coercions"}
+ Outer_Syntax.command @{command_keyword print_coercions}
"print information about coercions"
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
--- a/src/Tools/try.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/Tools/try.ML Mon Apr 06 23:24:45 2015 +0200
@@ -75,7 +75,7 @@
|> tap (fn NONE => writeln "Tried in vain." | _ => ())
val _ =
- Outer_Syntax.command @{command_spec "try"}
+ Outer_Syntax.command @{command_keyword 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/datatype_package.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon Apr 06 23:24:45 2015 +0200
@@ -430,7 +430,7 @@
val _ =
Outer_Syntax.command
- (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
+ (if coind then @{command_keyword codatatype} else @{command_keyword datatype})
("define " ^ coind_prefix ^ "datatype")
((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
--- a/src/ZF/Tools/ind_cases.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/ZF/Tools/ind_cases.ML Mon Apr 06 23:24:45 2015 +0200
@@ -53,7 +53,7 @@
in thy |> Global_Theory.note_thmss "" facts |> snd end;
val _ =
- Outer_Syntax.command @{command_spec "inductive_cases"}
+ Outer_Syntax.command @{command_keyword inductive_cases}
"create simplified instances of elimination rules (improper)"
(Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
>> (Toplevel.theory o inductive_cases));
--- a/src/ZF/Tools/induct_tacs.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Apr 06 23:24:45 2015 +0200
@@ -191,7 +191,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
+ Outer_Syntax.command @{command_keyword rep_datatype} "represent existing set inductively"
((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
(@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
(@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
--- a/src/ZF/Tools/inductive_package.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Mon Apr 06 23:24:45 2015 +0200
@@ -595,7 +595,7 @@
val _ =
Outer_Syntax.command
- (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
+ (if coind then @{command_keyword coinductive} else @{command_keyword inductive})
("define " ^ co_prefix ^ "inductive sets") ind_decl;
end;
--- a/src/ZF/Tools/primrec_package.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/ZF/Tools/primrec_package.ML Mon Apr 06 23:24:45 2015 +0200
@@ -197,7 +197,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
+ Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
(Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
>> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
--- a/src/ZF/Tools/typechk.ML Mon Apr 06 15:23:50 2015 +0200
+++ b/src/ZF/Tools/typechk.ML Mon Apr 06 23:24:45 2015 +0200
@@ -126,7 +126,7 @@
"ZF type-checking");
val _ =
- Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck"
+ Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (print_tcset o Toplevel.context_of)));