1.1 --- a/NEWS Fri Mar 16 16:32:34 2012 +0000
1.2 +++ b/NEWS Fri Mar 16 18:21:22 2012 +0100
1.3 @@ -379,6 +379,10 @@
1.4 * Antiquotation @{keyword "name"} produces a parser for outer syntax
1.5 from a minor keyword introduced via theory header declaration.
1.6
1.7 +* Antiquotation @{command_spec "name"} produces the
1.8 +Outer_Syntax.command_spec from a major keyword introduced via theory
1.9 +header declaration; it can be passed to Outer_Syntax.command etc.
1.10 +
1.11 * Local_Theory.define no longer hard-wires default theorem name
1.12 "foo_def": definitional packages need to make this explicit, and may
1.13 choose to omit theorem bindings for definitions by using
2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 16 16:32:34 2012 +0000
2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 16 18:21:22 2012 +0100
2.3 @@ -275,9 +275,8 @@
2.4 (Parse.string --| Args.colon -- Parse.nat))) []
2.5
2.6 val _ =
2.7 - Outer_Syntax.command "boogie_open"
2.8 + Outer_Syntax.command @{command_spec "boogie_open"}
2.9 "open a new Boogie environment and load a Boogie-generated .b2i file"
2.10 - Keyword.thy_decl
2.11 (scan_opt "quiet" -- Parse.name -- vc_offsets >>
2.12 (Toplevel.theory o boogie_open))
2.13
2.14 @@ -303,9 +302,8 @@
2.15 Scan.succeed VC_Complete
2.16
2.17 val _ =
2.18 - Outer_Syntax.command "boogie_vc"
2.19 + Outer_Syntax.command @{command_spec "boogie_vc"}
2.20 "enter into proof mode for a specific verification condition"
2.21 - Keyword.thy_goal
2.22 (vc_name -- vc_opts >> (fn args =>
2.23 (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
2.24
2.25 @@ -336,18 +334,16 @@
2.26 f (Toplevel.theory_of state))
2.27
2.28 val _ =
2.29 - Outer_Syntax.improper_command "boogie_status"
2.30 + Outer_Syntax.improper_command @{command_spec "boogie_status"}
2.31 "show the name and state of all loaded verification conditions"
2.32 - Keyword.diag
2.33 (status_test >> status_cmd ||
2.34 status_vc >> status_cmd ||
2.35 Scan.succeed (status_cmd boogie_status))
2.36
2.37
2.38 val _ =
2.39 - Outer_Syntax.command "boogie_end"
2.40 + Outer_Syntax.command @{command_spec "boogie_end"}
2.41 "close the current Boogie environment"
2.42 - Keyword.thy_decl
2.43 (Scan.succeed (Toplevel.theory boogie_end))
2.44
2.45
3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Fri Mar 16 16:32:34 2012 +0000
3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Fri Mar 16 18:21:22 2012 +0100
3.3 @@ -262,7 +262,7 @@
3.4 end
3.5
3.6 val _ =
3.7 - Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
3.8 - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain))
3.9 + Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
3.10 + (domains_decl >> (Toplevel.theory o mk_domain))
3.11
3.12 end
4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 16 16:32:34 2012 +0000
4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 16 18:21:22 2012 +0100
4.3 @@ -771,8 +771,7 @@
4.4 in
4.5
4.6 val _ =
4.7 - Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
4.8 - Keyword.thy_decl
4.9 + Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
4.10 (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
4.11
4.12 end
5.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Mar 16 16:32:34 2012 +0000
5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Mar 16 18:21:22 2012 +0100
5.3 @@ -357,14 +357,14 @@
5.4 ((def, the_default t opt_name), (t, args, mx), A, morphs)
5.5
5.6 val _ =
5.7 - Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
5.8 - Keyword.thy_goal
5.9 + Outer_Syntax.command @{command_spec "pcpodef"}
5.10 + "HOLCF type definition (requires admissibility proof)"
5.11 (typedef_proof_decl >>
5.12 (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
5.13
5.14 val _ =
5.15 - Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
5.16 - Keyword.thy_goal
5.17 + Outer_Syntax.command @{command_spec "cpodef"}
5.18 + "HOLCF type definition (requires admissibility proof)"
5.19 (typedef_proof_decl >>
5.20 (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
5.21
6.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Mar 16 16:32:34 2012 +0000
6.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Mar 16 18:21:22 2012 +0100
6.3 @@ -224,7 +224,7 @@
6.4 domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
6.5
6.6 val _ =
6.7 - Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl
6.8 + Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
6.9 (domaindef_decl >>
6.10 (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
6.11
7.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 16 16:32:34 2012 +0000
7.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 16 18:21:22 2012 +0100
7.3 @@ -402,7 +402,7 @@
7.4 in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
7.5
7.6 val _ =
7.7 - Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
7.8 + Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
7.9 (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
7.10 >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
7.11
8.1 --- a/src/HOL/Import/import.ML Fri Mar 16 16:32:34 2012 +0000
8.2 +++ b/src/HOL/Import/import.ML Fri Mar 16 18:21:22 2012 +0100
8.3 @@ -238,51 +238,43 @@
8.4 val append_dump = (Parse.verbatim || Parse.string) >> add_dump
8.5
8.6 val _ =
8.7 - (Outer_Syntax.command "import_segment"
8.8 - "Set import segment name"
8.9 - Keyword.thy_decl (import_segment >> Toplevel.theory);
8.10 - Outer_Syntax.command "import_theory"
8.11 - "Set default external theory name"
8.12 - Keyword.thy_decl (import_theory >> Toplevel.theory);
8.13 - Outer_Syntax.command "end_import"
8.14 - "End external import"
8.15 - Keyword.thy_decl (end_import >> Toplevel.theory);
8.16 - Outer_Syntax.command "setup_theory"
8.17 - "Setup external theory replaying"
8.18 - Keyword.thy_decl (setup_theory >> Toplevel.theory);
8.19 - Outer_Syntax.command "end_setup"
8.20 - "End external setup"
8.21 - Keyword.thy_decl (end_setup >> Toplevel.theory);
8.22 - Outer_Syntax.command "setup_dump"
8.23 - "Setup the dump file name"
8.24 - Keyword.thy_decl (set_dump >> Toplevel.theory);
8.25 - Outer_Syntax.command "append_dump"
8.26 - "Add text to dump file"
8.27 - Keyword.thy_decl (append_dump >> Toplevel.theory);
8.28 - Outer_Syntax.command "flush_dump"
8.29 - "Write the dump to file"
8.30 - Keyword.thy_decl (fl_dump >> Toplevel.theory);
8.31 - Outer_Syntax.command "ignore_thms"
8.32 - "Theorems to ignore in next external theory import"
8.33 - Keyword.thy_decl (ignore_thms >> Toplevel.theory);
8.34 - Outer_Syntax.command "type_maps"
8.35 - "Map external type names to existing Isabelle/HOL type names"
8.36 - Keyword.thy_decl (type_maps >> Toplevel.theory);
8.37 - Outer_Syntax.command "def_maps"
8.38 - "Map external constant names to their primitive definitions"
8.39 - Keyword.thy_decl (def_maps >> Toplevel.theory);
8.40 - Outer_Syntax.command "thm_maps"
8.41 - "Map external theorem names to existing Isabelle/HOL theorem names"
8.42 - Keyword.thy_decl (thm_maps >> Toplevel.theory);
8.43 - Outer_Syntax.command "const_renames"
8.44 - "Rename external const names"
8.45 - Keyword.thy_decl (const_renames >> Toplevel.theory);
8.46 - Outer_Syntax.command "const_moves"
8.47 - "Rename external const names to other external constants"
8.48 - Keyword.thy_decl (const_moves >> Toplevel.theory);
8.49 - Outer_Syntax.command "const_maps"
8.50 - "Map external const names to existing Isabelle/HOL const names"
8.51 - Keyword.thy_decl (const_maps >> Toplevel.theory));
8.52 + (Outer_Syntax.command @{command_spec "import_segment"} "set import segment name"
8.53 + (import_segment >> Toplevel.theory);
8.54 + Outer_Syntax.command @{command_spec "import_theory"} "set default external theory name"
8.55 + (import_theory >> Toplevel.theory);
8.56 + Outer_Syntax.command @{command_spec "end_import"} "end external import"
8.57 + (end_import >> Toplevel.theory);
8.58 + Outer_Syntax.command @{command_spec "setup_theory"} "setup external theory replaying"
8.59 + (setup_theory >> Toplevel.theory);
8.60 + Outer_Syntax.command @{command_spec "end_setup"} "end external setup"
8.61 + (end_setup >> Toplevel.theory);
8.62 + Outer_Syntax.command @{command_spec "setup_dump"} "setup the dump file name"
8.63 + (set_dump >> Toplevel.theory);
8.64 + Outer_Syntax.command @{command_spec "append_dump"} "add text to dump file"
8.65 + (append_dump >> Toplevel.theory);
8.66 + Outer_Syntax.command @{command_spec "flush_dump"} "write the dump to file"
8.67 + (fl_dump >> Toplevel.theory);
8.68 + Outer_Syntax.command @{command_spec "ignore_thms"}
8.69 + "theorems to ignore in next external theory import"
8.70 + (ignore_thms >> Toplevel.theory);
8.71 + Outer_Syntax.command @{command_spec "type_maps"}
8.72 + "map external type names to existing Isabelle/HOL type names"
8.73 + (type_maps >> Toplevel.theory);
8.74 + Outer_Syntax.command @{command_spec "def_maps"}
8.75 + "map external constant names to their primitive definitions"
8.76 + (def_maps >> Toplevel.theory);
8.77 + Outer_Syntax.command @{command_spec "thm_maps"}
8.78 + "map external theorem names to existing Isabelle/HOL theorem names"
8.79 + (thm_maps >> Toplevel.theory);
8.80 + Outer_Syntax.command @{command_spec "const_renames"}
8.81 + "rename external const names"
8.82 + (const_renames >> Toplevel.theory);
8.83 + Outer_Syntax.command @{command_spec "const_moves"}
8.84 + "rename external const names to other external constants"
8.85 + (const_moves >> Toplevel.theory);
8.86 + Outer_Syntax.command @{command_spec "const_maps"}
8.87 + "map external const names to existing Isabelle/HOL const names"
8.88 + (const_maps >> Toplevel.theory));
8.89
8.90 end
8.91
9.1 --- a/src/HOL/Nominal/nominal_atoms.ML Fri Mar 16 16:32:34 2012 +0000
9.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Fri Mar 16 18:21:22 2012 +0100
9.3 @@ -1016,7 +1016,7 @@
9.4 (* syntax und parsing *)
9.5
9.6 val _ =
9.7 - Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
9.8 + Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
9.9 (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
9.10
9.11 end;
10.1 --- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 16 16:32:34 2012 +0000
10.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 16 18:21:22 2012 +0100
10.3 @@ -2044,7 +2044,7 @@
10.4 val nominal_datatype_cmd = gen_nominal_datatype Datatype.read_specs;
10.5
10.6 val _ =
10.7 - Outer_Syntax.command "nominal_datatype" "define nominal datatypes" Keyword.thy_decl
10.8 + Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
10.9 (Parse.and_list1 Datatype.spec_cmd >>
10.10 (Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
10.11
11.1 --- a/src/HOL/Nominal/nominal_inductive.ML Fri Mar 16 16:32:34 2012 +0000
11.2 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Mar 16 18:21:22 2012 +0100
11.3 @@ -670,16 +670,15 @@
11.4 (* outer syntax *)
11.5
11.6 val _ =
11.7 - Outer_Syntax.local_theory_to_proof "nominal_inductive"
11.8 + Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
11.9 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
11.10 - Keyword.thy_goal
11.11 (Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
11.12 (@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
11.13 prove_strong_ind name avoids));
11.14
11.15 val _ =
11.16 - Outer_Syntax.local_theory "equivariance"
11.17 - "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
11.18 + Outer_Syntax.local_theory @{command_spec "equivariance"}
11.19 + "prove equivariance for inductive predicate involving nominal datatypes"
11.20 (Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
11.21 (fn (name, atoms) => prove_eqvt name atoms));
11.22
12.1 --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 16 16:32:34 2012 +0000
12.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 16 18:21:22 2012 +0100
12.3 @@ -484,9 +484,8 @@
12.4 (* outer syntax *)
12.5
12.6 val _ =
12.7 - Outer_Syntax.local_theory_to_proof "nominal_inductive2"
12.8 + Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
12.9 "prove strong induction theorem for inductive predicate involving nominal datatypes"
12.10 - Keyword.thy_goal
12.11 (Parse.xname --
12.12 Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
12.13 (Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
13.1 --- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 16 16:32:34 2012 +0000
13.2 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 16 18:21:22 2012 +0100
13.3 @@ -402,8 +402,8 @@
13.4 Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
13.5
13.6 val _ =
13.7 - Outer_Syntax.local_theory_to_proof "nominal_primrec"
13.8 - "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
13.9 + Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
13.10 + "define primitive recursive functions on nominal datatypes"
13.11 (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
13.12 >> (fn ((((invs, fctxt), fixes), params), specs) =>
13.13 add_primrec_cmd invs fctxt fixes params specs));
14.1 --- a/src/HOL/Orderings.thy Fri Mar 16 16:32:34 2012 +0000
14.2 +++ b/src/HOL/Orderings.thy Fri Mar 16 18:21:22 2012 +0100
14.3 @@ -409,8 +409,8 @@
14.4 (** Diagnostic command **)
14.5
14.6 val _ =
14.7 - Outer_Syntax.improper_command "print_orders"
14.8 - "print order structures available to transitivity reasoner" Keyword.diag
14.9 + Outer_Syntax.improper_command @{command_spec "print_orders"}
14.10 + "print order structures available to transitivity reasoner"
14.11 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
14.12 Toplevel.keep (print_structures o Toplevel.context_of)));
14.13
15.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Mar 16 16:32:34 2012 +0000
15.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Mar 16 18:21:22 2012 +0100
15.3 @@ -105,41 +105,36 @@
15.4 end);
15.5
15.6 val _ =
15.7 - Outer_Syntax.command "spark_open"
15.8 + Outer_Syntax.command @{command_spec "spark_open"}
15.9 "open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
15.10 - Keyword.thy_decl
15.11 (Parse.name -- Parse.parname >> (Toplevel.theory o spark_open));
15.12
15.13 val pfun_type = Scan.option
15.14 (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
15.15
15.16 val _ =
15.17 - Outer_Syntax.command "spark_proof_functions"
15.18 + Outer_Syntax.command @{command_spec "spark_proof_functions"}
15.19 "associate SPARK proof functions with terms"
15.20 - Keyword.thy_decl
15.21 (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
15.22 - (Toplevel.theory o fold add_proof_fun_cmd));
15.23 + (Toplevel.theory o fold add_proof_fun_cmd));
15.24
15.25 val _ =
15.26 - Outer_Syntax.command "spark_types"
15.27 + Outer_Syntax.command @{command_spec "spark_types"}
15.28 "associate SPARK types with types"
15.29 - Keyword.thy_decl
15.30 (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
15.31 Scan.optional (Args.parens (Parse.list1
15.32 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
15.33 (Toplevel.theory o fold add_spark_type_cmd));
15.34
15.35 val _ =
15.36 - Outer_Syntax.command "spark_vc"
15.37 + Outer_Syntax.command @{command_spec "spark_vc"}
15.38 "enter into proof mode for a specific verification condition"
15.39 - Keyword.thy_goal
15.40 (Parse.name >> (fn name =>
15.41 (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
15.42
15.43 val _ =
15.44 - Outer_Syntax.improper_command "spark_status"
15.45 + Outer_Syntax.improper_command @{command_spec "spark_status"}
15.46 "show the name and state of all loaded verification conditions"
15.47 - Keyword.diag
15.48 (Scan.optional
15.49 (Args.parens
15.50 ( Args.$$$ "proved" >> K (is_some, K "")
15.51 @@ -147,9 +142,8 @@
15.52 (K true, string_of_status) >> show_status);
15.53
15.54 val _ =
15.55 - Outer_Syntax.command "spark_end"
15.56 + Outer_Syntax.command @{command_spec "spark_end"}
15.57 "close the current SPARK environment"
15.58 - Keyword.thy_decl
15.59 (Scan.succeed (Toplevel.theory SPARK_VCs.close));
15.60
15.61 val setup = Theory.at_end (fn thy =>
16.1 --- a/src/HOL/Statespace/state_space.ML Fri Mar 16 16:32:34 2012 +0000
16.2 +++ b/src/HOL/Statespace/state_space.ML Fri Mar 16 18:21:22 2012 +0100
16.3 @@ -699,7 +699,7 @@
16.4 (plus1_unless comp parent --
16.5 Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
16.6 val _ =
16.7 - Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
16.8 + Outer_Syntax.command @{command_spec "statespace"} "define state space"
16.9 (statespace_decl >> (fn ((args, name), (parents, comps)) =>
16.10 Toplevel.theory (define_statespace args name parents comps)));
16.11
17.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Mar 16 16:32:34 2012 +0000
17.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Mar 16 18:21:22 2012 +0100
17.3 @@ -887,7 +887,7 @@
17.4 in TPTP_Data.map (cons ((prob_name, result))) thy' end
17.5
17.6 val _ =
17.7 - Outer_Syntax.improper_command "import_tptp" "import TPTP problem" Keyword.thy_decl
17.8 + Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
17.9 (Parse.path >> (fn path =>
17.10 Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
17.11
18.1 --- a/src/HOL/Tools/Datatype/datatype.ML Fri Mar 16 16:32:34 2012 +0000
18.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Mar 16 18:21:22 2012 +0100
18.3 @@ -792,7 +792,7 @@
18.4 >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
18.5
18.6 val _ =
18.7 - Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
18.8 + Outer_Syntax.command @{command_spec "datatype"} "define inductive datatypes"
18.9 (Parse.and_list1 spec_cmd
18.10 >> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config)));
18.11
19.1 --- a/src/HOL/Tools/Datatype/primrec.ML Fri Mar 16 16:32:34 2012 +0000
19.2 +++ b/src/HOL/Tools/Datatype/primrec.ML Fri Mar 16 18:21:22 2012 +0100
19.3 @@ -310,8 +310,8 @@
19.4 (* outer syntax *)
19.5
19.6 val _ =
19.7 - Outer_Syntax.local_theory "primrec" "define primitive recursive functions on datatypes"
19.8 - Keyword.thy_decl
19.9 + Outer_Syntax.local_theory @{command_spec "primrec"}
19.10 + "define primitive recursive functions on datatypes"
19.11 (Parse.fixes -- Parse_Spec.where_alt_specs
19.12 >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd));
19.13
20.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 16 16:32:34 2012 +0000
20.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 16 18:21:22 2012 +0100
20.3 @@ -643,7 +643,7 @@
20.4 (* outer syntax *)
20.5
20.6 val _ =
20.7 - Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
20.8 + Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
20.9 (Scan.repeat1 Parse.term >> (fn ts =>
20.10 Toplevel.print o
20.11 Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
21.1 --- a/src/HOL/Tools/Function/fun.ML Fri Mar 16 16:32:34 2012 +0000
21.2 +++ b/src/HOL/Tools/Function/fun.ML Fri Mar 16 18:21:22 2012 +0100
21.3 @@ -170,9 +170,9 @@
21.4
21.5
21.6 val _ =
21.7 - Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)"
21.8 - Keyword.thy_decl
21.9 - (function_parser fun_config
21.10 - >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
21.11 + Outer_Syntax.local_theory' @{command_spec "fun"}
21.12 + "define general recursive functions (short version)"
21.13 + (function_parser fun_config
21.14 + >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
21.15
21.16 end
22.1 --- a/src/HOL/Tools/Function/function.ML Fri Mar 16 16:32:34 2012 +0000
22.2 +++ b/src/HOL/Tools/Function/function.ML Fri Mar 16 18:21:22 2012 +0100
22.3 @@ -277,15 +277,15 @@
22.4 (* outer syntax *)
22.5
22.6 val _ =
22.7 - Outer_Syntax.local_theory_to_proof' "function" "define general recursive functions"
22.8 - Keyword.thy_goal
22.9 - (function_parser default_config
22.10 - >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
22.11 + Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
22.12 + "define general recursive functions"
22.13 + (function_parser default_config
22.14 + >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
22.15
22.16 val _ =
22.17 - Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
22.18 - Keyword.thy_goal
22.19 - (Scan.option Parse.term >> termination_cmd)
22.20 + Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
22.21 + "prove termination of a recursive function"
22.22 + (Scan.option Parse.term >> termination_cmd)
22.23
22.24
22.25 end
23.1 --- a/src/HOL/Tools/Function/partial_function.ML Fri Mar 16 16:32:34 2012 +0000
23.2 +++ b/src/HOL/Tools/Function/partial_function.ML Fri Mar 16 18:21:22 2012 +0100
23.3 @@ -281,10 +281,10 @@
23.4
23.5 val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
23.6
23.7 -val _ = Outer_Syntax.local_theory
23.8 - "partial_function" "define partial function" Keyword.thy_decl
23.9 - ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
23.10 - >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
23.11 +val _ =
23.12 + Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
23.13 + ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
23.14 + >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
23.15
23.16
23.17 val setup = Mono_Rules.setup;
24.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 16 16:32:34 2012 +0000
24.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 16 18:21:22 2012 +0100
24.3 @@ -390,16 +390,15 @@
24.4 params |> map string_for_raw_param
24.5 |> sort_strings |> cat_lines)))))
24.6
24.7 -val parse_nitpick_command =
24.8 - (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
24.9 -val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
24.10 +val _ =
24.11 + Outer_Syntax.improper_command @{command_spec "nitpick"}
24.12 + "try to find a counterexample for a given subgoal using Nitpick"
24.13 + ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans)
24.14
24.15 -val _ = Outer_Syntax.improper_command nitpickN
24.16 - "try to find a counterexample for a given subgoal using Nitpick"
24.17 - Keyword.diag parse_nitpick_command
24.18 -val _ = Outer_Syntax.command nitpick_paramsN
24.19 - "set and display the default parameters for Nitpick"
24.20 - Keyword.thy_decl parse_nitpick_params_command
24.21 +val _ =
24.22 + Outer_Syntax.command @{command_spec "nitpick_params"}
24.23 + "set and display the default parameters for Nitpick"
24.24 + (parse_params #>> nitpick_params_trans)
24.25
24.26 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
24.27
25.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 16 16:32:34 2012 +0000
25.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 16 18:21:22 2012 +0100
25.3 @@ -1004,10 +1004,13 @@
25.4 val opt_print_modes =
25.5 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
25.6
25.7 -val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
25.8 - (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
25.9 - >> (fn ((print_modes, soln), t) => Toplevel.keep
25.10 - (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
25.11 +val _ =
25.12 + Outer_Syntax.improper_command @{command_spec "values"}
25.13 + "enumerate and print comprehensions"
25.14 + (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
25.15 + >> (fn ((print_modes, soln), t) => Toplevel.keep
25.16 + (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
25.17 +
25.18
25.19 (* quickcheck generator *)
25.20
26.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Mar 16 16:32:34 2012 +0000
26.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Mar 16 18:21:22 2012 +0100
26.3 @@ -270,14 +270,16 @@
26.4
26.5 (* code_pred command and values command *)
26.6
26.7 -val _ = Outer_Syntax.local_theory_to_proof "code_pred"
26.8 - "prove equations for predicate specified by intro/elim rules"
26.9 - Keyword.thy_goal
26.10 - (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
26.11 +val _ =
26.12 + Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
26.13 + "prove equations for predicate specified by intro/elim rules"
26.14 + (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
26.15
26.16 -val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
26.17 - (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
26.18 - >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
26.19 - (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
26.20 +val _ =
26.21 + Outer_Syntax.improper_command @{command_spec "values"}
26.22 + "enumerate and print comprehensions"
26.23 + (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
26.24 + >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
26.25 + (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)))
26.26
26.27 end
27.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Fri Mar 16 16:32:34 2012 +0000
27.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Fri Mar 16 18:21:22 2012 +0100
27.3 @@ -64,8 +64,10 @@
27.4 val quickcheck_generator_cmd = gen_quickcheck_generator
27.5 (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
27.6
27.7 -val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
27.8 - Keyword.thy_decl ((Parse.type_const --
27.9 +val _ =
27.10 + Outer_Syntax.command @{command_spec "quickcheck_generator"}
27.11 + "define quickcheck generators for abstract types"
27.12 + ((Parse.type_const --
27.13 Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
27.14 (Args.$$$ "constructors" |-- @{keyword ":"} |-- Parse.list1 Parse.term)
27.15 >> (fn ((tyco, opt_pred), constrs) =>
28.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Fri Mar 16 16:32:34 2012 +0000
28.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Fri Mar 16 18:21:22 2012 +0100
28.3 @@ -104,8 +104,8 @@
28.4
28.5
28.6 val _ =
28.7 - Outer_Syntax.improper_command "find_unused_assms" "find theorems with superfluous assumptions"
28.8 - Keyword.diag
28.9 + Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
28.10 + "find theorems with superfluous assumptions"
28.11 (Scan.option Parse.name
28.12 >> (fn opt_thy_name =>
28.13 Toplevel.no_timing o Toplevel.keep (fn state =>
29.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 16 16:32:34 2012 +0000
29.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 16 18:21:22 2012 +0100
29.3 @@ -106,14 +106,13 @@
29.4 quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
29.5 end
29.6
29.7 -(* parser and command *)
29.8 -val quotdef_parser =
29.9 - Scan.option Parse_Spec.constdecl --
29.10 - Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
29.11 +(* command *)
29.12
29.13 val _ =
29.14 - Outer_Syntax.local_theory "quotient_definition"
29.15 + Outer_Syntax.local_theory @{command_spec "quotient_definition"}
29.16 "definition for constants over the quotient type"
29.17 - Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
29.18 + (Scan.option Parse_Spec.constdecl --
29.19 + Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
29.20 + >> (snd oo quotient_def_cmd))
29.21
29.22 end; (* structure *)
30.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 16 16:32:34 2012 +0000
30.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 16 18:21:22 2012 +0100
30.3 @@ -291,15 +291,15 @@
30.4 (* outer syntax commands *)
30.5
30.6 val _ =
30.7 - Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
30.8 + Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
30.9 (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
30.10
30.11 val _ =
30.12 - Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
30.13 + Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
30.14 (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
30.15
30.16 val _ =
30.17 - Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
30.18 + Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
30.19 (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
30.20
30.21 end;
31.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 16 16:32:34 2012 +0000
31.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 16 18:21:22 2012 +0100
31.3 @@ -264,17 +264,15 @@
31.4
31.5 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
31.6
31.7 -val quotspec_parser =
31.8 - Parse.and_list1
31.9 - ((Parse.type_args -- Parse.binding) --
31.10 - (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
31.11 - Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
31.12 - (@{keyword "/"} |-- (partial -- Parse.term)) --
31.13 - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
31.14 -
31.15 val _ =
31.16 - Outer_Syntax.local_theory_to_proof "quotient_type"
31.17 + Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
31.18 "quotient type definitions (require equivalence proofs)"
31.19 - Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
31.20 + (Parse.and_list1
31.21 + ((Parse.type_args -- Parse.binding) --
31.22 + (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
31.23 + Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
31.24 + (@{keyword "/"} |-- (partial -- Parse.term)) --
31.25 + Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
31.26 + >> quotient_type_cmd)
31.27
31.28 end;
32.1 --- a/src/HOL/Tools/SMT/smt_config.ML Fri Mar 16 16:32:34 2012 +0000
32.2 +++ b/src/HOL/Tools/SMT/smt_config.ML Fri Mar 16 18:21:22 2012 +0100
32.3 @@ -247,10 +247,9 @@
32.4 end
32.5
32.6 val _ =
32.7 - Outer_Syntax.improper_command "smt_status"
32.8 - ("show the available SMT solvers, the currently selected SMT solver, " ^
32.9 - "and the values of SMT configuration options")
32.10 - Keyword.diag
32.11 + Outer_Syntax.improper_command @{command_spec "smt_status"}
32.12 + "show the available SMT solvers, the currently selected SMT solver, \
32.13 + \and the values of SMT configuration options"
32.14 (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
32.15 print_setup (Toplevel.context_of state))))
32.16
33.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 16 16:32:34 2012 +0000
33.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 16 18:21:22 2012 +0100
33.3 @@ -413,20 +413,16 @@
33.4 Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
33.5 >> merge_relevance_overrides))
33.6 no_relevance_override
33.7 -val parse_sledgehammer_command =
33.8 - (Scan.optional Parse.short_ident runN -- parse_params
33.9 - -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
33.10 -val parse_sledgehammer_params_command =
33.11 - parse_params #>> sledgehammer_params_trans
33.12
33.13 val _ =
33.14 - Outer_Syntax.improper_command sledgehammerN
33.15 - "search for first-order proof using automatic theorem provers" Keyword.diag
33.16 - parse_sledgehammer_command
33.17 + Outer_Syntax.improper_command @{command_spec "sledgehammer"}
33.18 + "search for first-order proof using automatic theorem provers"
33.19 + ((Scan.optional Parse.short_ident runN -- parse_params
33.20 + -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
33.21 val _ =
33.22 - Outer_Syntax.command sledgehammer_paramsN
33.23 - "set and display the default parameters for Sledgehammer" Keyword.thy_decl
33.24 - parse_sledgehammer_params_command
33.25 + Outer_Syntax.command @{command_spec "sledgehammer_params"}
33.26 + "set and display the default parameters for Sledgehammer"
33.27 + (parse_params #>> sledgehammer_params_trans)
33.28
33.29 fun try_sledgehammer auto state =
33.30 let
34.1 --- a/src/HOL/Tools/choice_specification.ML Fri Mar 16 16:32:34 2012 +0000
34.2 +++ b/src/HOL/Tools/choice_specification.ML Fri Mar 16 18:21:22 2012 +0100
34.3 @@ -237,25 +237,19 @@
34.4 val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
34.5 val opt_overloaded = Parse.opt_keyword "overloaded"
34.6
34.7 -val specification_decl =
34.8 - @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
34.9 - Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
34.10 +val _ =
34.11 + Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
34.12 + (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
34.13 + Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
34.14 + >> (fn (cos, alt_props) => Toplevel.print o
34.15 + (Toplevel.theory_to_proof (process_spec NONE cos alt_props))))
34.16
34.17 val _ =
34.18 - Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
34.19 - (specification_decl >> (fn (cos,alt_props) =>
34.20 - Toplevel.print o (Toplevel.theory_to_proof
34.21 - (process_spec NONE cos alt_props))))
34.22 -
34.23 -val ax_specification_decl =
34.24 - Parse.name --
34.25 - (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
34.26 - Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
34.27 -
34.28 -val _ =
34.29 - Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
34.30 - (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
34.31 - Toplevel.print o (Toplevel.theory_to_proof
34.32 - (process_spec (SOME axname) cos alt_props))))
34.33 + Outer_Syntax.command @{command_spec "ax_specification"} "define constants by specification"
34.34 + (Parse.name --
34.35 + (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
34.36 + Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
34.37 + >> (fn (axname, (cos, alt_props)) =>
34.38 + Toplevel.print o (Toplevel.theory_to_proof (process_spec (SOME axname) cos alt_props))))
34.39
34.40 end
35.1 --- a/src/HOL/Tools/enriched_type.ML Fri Mar 16 16:32:34 2012 +0000
35.2 +++ b/src/HOL/Tools/enriched_type.ML Fri Mar 16 18:21:22 2012 +0100
35.3 @@ -266,9 +266,10 @@
35.4 val enriched_type = gen_enriched_type Syntax.check_term;
35.5 val enriched_type_cmd = gen_enriched_type Syntax.read_term;
35.6
35.7 -val _ = Outer_Syntax.local_theory_to_proof "enriched_type"
35.8 - "register operations managing the functorial structure of a type"
35.9 - Keyword.thy_goal (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
35.10 - >> (fn (prfx, t) => enriched_type_cmd prfx t));
35.11 +val _ =
35.12 + Outer_Syntax.local_theory_to_proof @{command_spec "enriched_type"}
35.13 + "register operations managing the functorial structure of a type"
35.14 + (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
35.15 + >> (fn (prfx, t) => enriched_type_cmd prfx t));
35.16
35.17 end;
36.1 --- a/src/HOL/Tools/inductive.ML Fri Mar 16 16:32:34 2012 +0000
36.2 +++ b/src/HOL/Tools/inductive.ML Fri Mar 16 18:21:22 2012 +0100
36.3 @@ -1144,21 +1144,21 @@
36.4 val ind_decl = gen_ind_decl add_ind_def;
36.5
36.6 val _ =
36.7 - Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
36.8 + Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
36.9 (ind_decl false);
36.10
36.11 val _ =
36.12 - Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
36.13 + Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
36.14 (ind_decl true);
36.15
36.16 val _ =
36.17 - Outer_Syntax.local_theory "inductive_cases"
36.18 - "create simplified instances of elimination rules (improper)" Keyword.thy_script
36.19 + Outer_Syntax.local_theory @{command_spec "inductive_cases"}
36.20 + "create simplified instances of elimination rules (improper)"
36.21 (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
36.22
36.23 val _ =
36.24 - Outer_Syntax.local_theory "inductive_simps"
36.25 - "create simplification rules for inductive predicates" Keyword.thy_script
36.26 + Outer_Syntax.local_theory @{command_spec "inductive_simps"}
36.27 + "create simplification rules for inductive predicates"
36.28 (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
36.29
36.30 end;
37.1 --- a/src/HOL/Tools/inductive_set.ML Fri Mar 16 16:32:34 2012 +0000
37.2 +++ b/src/HOL/Tools/inductive_set.ML Fri Mar 16 18:21:22 2012 +0100
37.3 @@ -575,11 +575,11 @@
37.4 val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
37.5
37.6 val _ =
37.7 - Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
37.8 + Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
37.9 (ind_set_decl false);
37.10
37.11 val _ =
37.12 - Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
37.13 + Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
37.14 (ind_set_decl true);
37.15
37.16 end;
38.1 --- a/src/HOL/Tools/recdef.ML Fri Mar 16 16:32:34 2012 +0000
38.2 +++ b/src/HOL/Tools/recdef.ML Fri Mar 16 18:21:22 2012 +0100
38.3 @@ -302,7 +302,7 @@
38.4 >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
38.5
38.6 val _ =
38.7 - Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
38.8 + Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
38.9 (recdef_decl >> Toplevel.theory);
38.10
38.11
38.12 @@ -313,12 +313,13 @@
38.13 >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
38.14
38.15 val _ =
38.16 - Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
38.17 + Outer_Syntax.command @{command_spec "defer_recdef"}
38.18 + "defer general recursive functions (TFL)"
38.19 (defer_recdef_decl >> Toplevel.theory);
38.20
38.21 val _ =
38.22 - Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
38.23 - Keyword.thy_goal
38.24 + Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
38.25 + "recommence proof of termination condition (TFL)"
38.26 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
38.27 Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
38.28 >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
39.1 --- a/src/HOL/Tools/record.ML Fri Mar 16 16:32:34 2012 +0000
39.2 +++ b/src/HOL/Tools/record.ML Fri Mar 16 18:21:22 2012 +0100
39.3 @@ -2311,7 +2311,7 @@
39.4 (* outer syntax *)
39.5
39.6 val _ =
39.7 - Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
39.8 + Outer_Syntax.command @{command_spec "record"} "define extensible record"
39.9 (Parse.type_args_constrained -- Parse.binding --
39.10 (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
39.11 Scan.repeat1 Parse.const_binding)
40.1 --- a/src/HOL/Tools/refute.ML Fri Mar 16 16:32:34 2012 +0000
40.2 +++ b/src/HOL/Tools/refute.ML Fri Mar 16 18:21:22 2012 +0100
40.3 @@ -3198,8 +3198,8 @@
40.4 (* 'refute' command *)
40.5
40.6 val _ =
40.7 - Outer_Syntax.improper_command "refute"
40.8 - "try to find a model that refutes a given subgoal" Keyword.diag
40.9 + Outer_Syntax.improper_command @{command_spec "refute"}
40.10 + "try to find a model that refutes a given subgoal"
40.11 (scan_parms -- Scan.optional Parse.nat 1 >>
40.12 (fn (parms, i) =>
40.13 Toplevel.keep (fn state =>
40.14 @@ -3212,8 +3212,8 @@
40.15 (* 'refute_params' command *)
40.16
40.17 val _ =
40.18 - Outer_Syntax.command "refute_params"
40.19 - "show/store default parameters for the 'refute' command" Keyword.thy_decl
40.20 + Outer_Syntax.command @{command_spec "refute_params"}
40.21 + "show/store default parameters for the 'refute' command"
40.22 (scan_parms >> (fn parms =>
40.23 Toplevel.theory (fn thy =>
40.24 let
41.1 --- a/src/HOL/Tools/try0.ML Fri Mar 16 16:32:34 2012 +0000
41.2 +++ b/src/HOL/Tools/try0.ML Fri Mar 16 18:21:22 2012 +0100
41.3 @@ -183,13 +183,10 @@
41.4 || Scan.repeat parse_attr
41.5 >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
41.6
41.7 -val parse_try0_command =
41.8 - Scan.optional parse_attrs ([], [], [], []) #>> try0_trans
41.9 -
41.10 val _ =
41.11 - Outer_Syntax.improper_command try0N
41.12 - "try a combination of proof methods" Keyword.diag
41.13 - parse_try0_command
41.14 + Outer_Syntax.improper_command @{command_spec "try0"}
41.15 + "try a combination of proof methods"
41.16 + (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans)
41.17
41.18 fun try_try0 auto =
41.19 do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
42.1 --- a/src/HOL/Tools/typedef.ML Fri Mar 16 16:32:34 2012 +0000
42.2 +++ b/src/HOL/Tools/typedef.ML Fri Mar 16 18:21:22 2012 +0100
42.3 @@ -300,8 +300,8 @@
42.4 (** outer syntax **)
42.5
42.6 val _ =
42.7 - Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
42.8 - Keyword.thy_goal
42.9 + Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
42.10 + "HOL type definition (requires non-emptiness proof)"
42.11 (Scan.optional (@{keyword "("} |--
42.12 ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
42.13 Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
43.1 --- a/src/Provers/classical.ML Fri Mar 16 16:32:34 2012 +0000
43.2 +++ b/src/Provers/classical.ML Fri Mar 16 18:21:22 2012 +0100
43.3 @@ -960,8 +960,7 @@
43.4 (** outer syntax **)
43.5
43.6 val _ =
43.7 - Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
43.8 - Keyword.diag
43.9 + Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
43.10 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
43.11 Toplevel.keep (fn state =>
43.12 let val ctxt = Toplevel.context_of state
44.1 --- a/src/Pure/Isar/isar_syn.ML Fri Mar 16 16:32:34 2012 +0000
44.2 +++ b/src/Pure/Isar/isar_syn.ML Fri Mar 16 18:21:22 2012 +0100
44.3 @@ -25,14 +25,14 @@
44.4 (** init and exit **)
44.5
44.6 val _ =
44.7 - Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
44.8 + Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
44.9 (Thy_Header.args >> (fn header =>
44.10 Toplevel.print o
44.11 Toplevel.init_theory
44.12 (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
44.13
44.14 val _ =
44.15 - Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
44.16 + Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
44.17 (Scan.succeed
44.18 (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
44.19
44.20 @@ -40,43 +40,65 @@
44.21
44.22 (** markup commands **)
44.23
44.24 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
44.25 - (Parse.doc_source >> Isar_Cmd.header_markup);
44.26 -
44.27 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
44.28 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.29 -
44.30 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
44.31 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.32 -
44.33 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
44.34 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.35 +val _ =
44.36 + Outer_Syntax.markup_command Thy_Output.Markup
44.37 + ("header", Keyword.diag) "theory header"
44.38 + (Parse.doc_source >> Isar_Cmd.header_markup);
44.39
44.40 val _ =
44.41 - Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
44.42 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.43 + Outer_Syntax.markup_command Thy_Output.Markup
44.44 + ("chapter", Keyword.thy_heading) "chapter heading"
44.45 + (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.46
44.47 -val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
44.48 - Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.49 +val _ =
44.50 + Outer_Syntax.markup_command Thy_Output.Markup
44.51 + ("section", Keyword.thy_heading) "section heading"
44.52 + (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.53
44.54 -val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
44.55 - Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.56 +val _ =
44.57 + Outer_Syntax.markup_command Thy_Output.Markup
44.58 + ("subsection", Keyword.thy_heading) "subsection heading"
44.59 + (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.60
44.61 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
44.62 - (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
44.63 +val _ =
44.64 + Outer_Syntax.markup_command Thy_Output.Markup
44.65 + ("subsubsection", Keyword.thy_heading) "subsubsection heading"
44.66 + (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.67
44.68 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
44.69 - (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
44.70 +val _ =
44.71 + Outer_Syntax.markup_command Thy_Output.MarkupEnv
44.72 + ("text", Keyword.thy_decl) "formal comment (theory)"
44.73 + (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.74
44.75 -val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
44.76 - (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
44.77 +val _ =
44.78 + Outer_Syntax.markup_command Thy_Output.Verbatim
44.79 + ("text_raw", Keyword.thy_decl) "raw document preparation text"
44.80 + (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
44.81
44.82 -val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
44.83 - (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
44.84 +val _ =
44.85 + Outer_Syntax.markup_command Thy_Output.Markup
44.86 + ("sect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
44.87 + (Parse.doc_source >> Isar_Cmd.proof_markup);
44.88
44.89 -val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
44.90 - "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
44.91 - (Parse.doc_source >> Isar_Cmd.proof_markup);
44.92 +val _ =
44.93 + Outer_Syntax.markup_command Thy_Output.Markup
44.94 + ("subsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
44.95 + (Parse.doc_source >> Isar_Cmd.proof_markup);
44.96 +
44.97 +val _ =
44.98 + Outer_Syntax.markup_command Thy_Output.Markup
44.99 + ("subsubsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
44.100 + (Parse.doc_source >> Isar_Cmd.proof_markup);
44.101 +
44.102 +val _ =
44.103 + Outer_Syntax.markup_command Thy_Output.MarkupEnv
44.104 + ("txt", Keyword.tag_proof Keyword.prf_decl) "formal comment (proof)"
44.105 + (Parse.doc_source >> Isar_Cmd.proof_markup);
44.106 +
44.107 +val _ =
44.108 + Outer_Syntax.markup_command Thy_Output.Verbatim
44.109 + ("txt_raw", Keyword.tag_proof Keyword.prf_decl) "raw document preparation text (proof)"
44.110 + (Parse.doc_source >> Isar_Cmd.proof_markup);
44.111
44.112
44.113
44.114 @@ -85,60 +107,60 @@
44.115 (* classes and sorts *)
44.116
44.117 val _ =
44.118 - Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
44.119 + Outer_Syntax.command ("classes", Keyword.thy_decl) "declare type classes"
44.120 (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
44.121 Parse.!!! (Parse.list1 Parse.class)) [])
44.122 >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
44.123
44.124 val _ =
44.125 - Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
44.126 + Outer_Syntax.command ("classrel", Keyword.thy_decl) "state inclusion of type classes (axiomatic!)"
44.127 (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
44.128 |-- Parse.!!! Parse.class))
44.129 >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
44.130
44.131 val _ =
44.132 - Outer_Syntax.local_theory "default_sort" "declare default sort for explicit type variables"
44.133 - Keyword.thy_decl
44.134 + Outer_Syntax.local_theory ("default_sort", Keyword.thy_decl)
44.135 + "declare default sort for explicit type variables"
44.136 (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
44.137
44.138
44.139 (* types *)
44.140
44.141 val _ =
44.142 - Outer_Syntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
44.143 + Outer_Syntax.local_theory ("typedecl", Keyword.thy_decl) "type declaration"
44.144 (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
44.145 >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
44.146
44.147 val _ =
44.148 - Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
44.149 + Outer_Syntax.local_theory ("type_synonym", Keyword.thy_decl) "declare type abbreviation"
44.150 (Parse.type_args -- Parse.binding --
44.151 (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
44.152 >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
44.153
44.154 val _ =
44.155 - Outer_Syntax.command "nonterminal"
44.156 - "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
44.157 + Outer_Syntax.command ("nonterminal", Keyword.thy_decl)
44.158 + "declare syntactic type constructors (grammar nonterminal symbols)"
44.159 (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
44.160
44.161 val _ =
44.162 - Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
44.163 + Outer_Syntax.command ("arities", Keyword.thy_decl) "state type arities (axiomatic!)"
44.164 (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
44.165
44.166
44.167 (* consts and syntax *)
44.168
44.169 val _ =
44.170 - Outer_Syntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
44.171 + Outer_Syntax.command ("judgment", Keyword.thy_decl) "declare object-logic judgment"
44.172 (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
44.173
44.174 val _ =
44.175 - Outer_Syntax.command "consts" "declare constants" Keyword.thy_decl
44.176 + Outer_Syntax.command ("consts", Keyword.thy_decl) "declare constants"
44.177 (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
44.178
44.179 val opt_overloaded = Parse.opt_keyword "overloaded";
44.180
44.181 val _ =
44.182 - Outer_Syntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
44.183 + Outer_Syntax.command ("finalconsts", Keyword.thy_decl) "declare constants as final"
44.184 (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
44.185
44.186 val mode_spec =
44.187 @@ -149,11 +171,11 @@
44.188 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
44.189
44.190 val _ =
44.191 - Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
44.192 + Outer_Syntax.command ("syntax", Keyword.thy_decl) "declare syntactic constants"
44.193 (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
44.194
44.195 val _ =
44.196 - Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
44.197 + Outer_Syntax.command ("no_syntax", Keyword.thy_decl) "delete syntax declarations"
44.198 (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
44.199
44.200
44.201 @@ -174,18 +196,18 @@
44.202 >> (fn (left, (arr, right)) => arr (left, right));
44.203
44.204 val _ =
44.205 - Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
44.206 + Outer_Syntax.command ("translations", Keyword.thy_decl) "declare syntax translation rules"
44.207 (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
44.208
44.209 val _ =
44.210 - Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
44.211 + Outer_Syntax.command ("no_translations", Keyword.thy_decl) "remove syntax translation rules"
44.212 (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
44.213
44.214
44.215 (* axioms and definitions *)
44.216
44.217 val _ =
44.218 - Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
44.219 + Outer_Syntax.command ("axioms", Keyword.thy_decl) "state arbitrary propositions (axiomatic!)"
44.220 (Scan.repeat1 Parse_Spec.spec >>
44.221 (fn spec => Toplevel.theory (fn thy =>
44.222 (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
44.223 @@ -197,7 +219,7 @@
44.224 Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
44.225
44.226 val _ =
44.227 - Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
44.228 + Outer_Syntax.command ("defs", Keyword.thy_decl) "define constants"
44.229 (opt_unchecked_overloaded --
44.230 Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
44.231 >> (Toplevel.theory o Isar_Cmd.add_defs));
44.232 @@ -206,35 +228,35 @@
44.233 (* constant definitions and abbreviations *)
44.234
44.235 val _ =
44.236 - Outer_Syntax.local_theory' "definition" "constant definition" Keyword.thy_decl
44.237 + Outer_Syntax.local_theory' ("definition", Keyword.thy_decl) "constant definition"
44.238 (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
44.239
44.240 val _ =
44.241 - Outer_Syntax.local_theory' "abbreviation" "constant abbreviation" Keyword.thy_decl
44.242 + Outer_Syntax.local_theory' ("abbreviation", Keyword.thy_decl) "constant abbreviation"
44.243 (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
44.244 >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
44.245
44.246 val _ =
44.247 - Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
44.248 - Keyword.thy_decl
44.249 + Outer_Syntax.local_theory ("type_notation", Keyword.thy_decl)
44.250 + "add concrete syntax for type constructors"
44.251 (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
44.252 >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
44.253
44.254 val _ =
44.255 - Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
44.256 - Keyword.thy_decl
44.257 + Outer_Syntax.local_theory ("no_type_notation", Keyword.thy_decl)
44.258 + "delete concrete syntax for type constructors"
44.259 (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
44.260 >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
44.261
44.262 val _ =
44.263 - Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
44.264 - Keyword.thy_decl
44.265 + Outer_Syntax.local_theory ("notation", Keyword.thy_decl)
44.266 + "add concrete syntax for constants / fixed variables"
44.267 (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
44.268 >> (fn (mode, args) => Specification.notation_cmd true mode args));
44.269
44.270 val _ =
44.271 - Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
44.272 - Keyword.thy_decl
44.273 + Outer_Syntax.local_theory ("no_notation", Keyword.thy_decl)
44.274 + "delete concrete syntax for constants / fixed variables"
44.275 (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
44.276 >> (fn (mode, args) => Specification.notation_cmd false mode args));
44.277
44.278 @@ -242,7 +264,7 @@
44.279 (* constant specifications *)
44.280
44.281 val _ =
44.282 - Outer_Syntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
44.283 + Outer_Syntax.command ("axiomatization", Keyword.thy_decl) "axiomatic constant specification"
44.284 (Scan.optional Parse.fixes [] --
44.285 Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
44.286 >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
44.287 @@ -255,13 +277,14 @@
44.288 >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
44.289
44.290 val _ =
44.291 - Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
44.292 + Outer_Syntax.local_theory' ("theorems", Keyword.thy_decl) "define theorems"
44.293 + (theorems Thm.theoremK);
44.294
44.295 val _ =
44.296 - Outer_Syntax.local_theory' "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
44.297 + Outer_Syntax.local_theory' ("lemmas", Keyword.thy_decl) "define lemmas" (theorems Thm.lemmaK);
44.298
44.299 val _ =
44.300 - Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl
44.301 + Outer_Syntax.local_theory' ("declare", Keyword.thy_decl) "declare theorems"
44.302 (Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
44.303 >> (fn (facts, fixes) =>
44.304 #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
44.305 @@ -270,7 +293,7 @@
44.306 (* name space entry path *)
44.307
44.308 fun hide_names name hide what =
44.309 - Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
44.310 + Outer_Syntax.command (name, Keyword.thy_decl) ("hide " ^ what ^ " from name space")
44.311 ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
44.312 (Toplevel.theory o uncurry hide));
44.313
44.314 @@ -283,65 +306,66 @@
44.315 (* use ML text *)
44.316
44.317 val _ =
44.318 - Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
44.319 + Outer_Syntax.command ("use", Keyword.tag_ml Keyword.thy_decl) "ML text from file"
44.320 (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
44.321
44.322 val _ =
44.323 - Outer_Syntax.command "ML" "ML text within theory or local theory"
44.324 - (Keyword.tag_ml Keyword.thy_decl)
44.325 + Outer_Syntax.command ("ML", Keyword.tag_ml Keyword.thy_decl)
44.326 + "ML text within theory or local theory"
44.327 (Parse.ML_source >> (fn (txt, pos) =>
44.328 Toplevel.generic_theory
44.329 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
44.330 Local_Theory.propagate_ml_env)));
44.331
44.332 val _ =
44.333 - Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
44.334 + Outer_Syntax.command ("ML_prf", Keyword.tag_proof Keyword.prf_decl) "ML text within proof"
44.335 (Parse.ML_source >> (fn (txt, pos) =>
44.336 Toplevel.proof (Proof.map_context (Context.proof_map
44.337 (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
44.338
44.339 val _ =
44.340 - Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
44.341 + Outer_Syntax.command ("ML_val", Keyword.tag_ml Keyword.diag) "diagnostic ML text"
44.342 (Parse.ML_source >> Isar_Cmd.ml_diag true);
44.343
44.344 val _ =
44.345 - Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
44.346 + Outer_Syntax.command ("ML_command", Keyword.tag_ml Keyword.diag) "diagnostic ML text (silent)"
44.347 (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
44.348
44.349 val _ =
44.350 - Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
44.351 + Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup"
44.352 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
44.353
44.354 val _ =
44.355 - Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
44.356 + Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup"
44.357 (Parse.ML_source >> Isar_Cmd.local_setup);
44.358
44.359 val _ =
44.360 - Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
44.361 + Outer_Syntax.command ("attribute_setup", Keyword.tag_ml Keyword.thy_decl) "define attribute in ML"
44.362 (Parse.position Parse.name --
44.363 Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
44.364 >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
44.365
44.366 val _ =
44.367 - Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
44.368 + Outer_Syntax.command ("method_setup", Keyword.tag_ml Keyword.thy_decl) "define proof method in ML"
44.369 (Parse.position Parse.name --
44.370 Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
44.371 >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
44.372
44.373 val _ =
44.374 - Outer_Syntax.local_theory "declaration" "generic ML declaration"
44.375 - (Keyword.tag_ml Keyword.thy_decl)
44.376 + Outer_Syntax.local_theory ("declaration", Keyword.tag_ml Keyword.thy_decl)
44.377 + "generic ML declaration"
44.378 (Parse.opt_keyword "pervasive" -- Parse.ML_source
44.379 >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
44.380
44.381 val _ =
44.382 - Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
44.383 - (Keyword.tag_ml Keyword.thy_decl)
44.384 + Outer_Syntax.local_theory ("syntax_declaration", Keyword.tag_ml Keyword.thy_decl)
44.385 + "generic ML declaration"
44.386 (Parse.opt_keyword "pervasive" -- Parse.ML_source
44.387 >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
44.388
44.389 val _ =
44.390 - Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
44.391 + Outer_Syntax.local_theory ("simproc_setup", Keyword.tag_ml Keyword.thy_decl)
44.392 + "define simproc in ML"
44.393 (Parse.position Parse.name --
44.394 (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
44.395 Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
44.396 @@ -353,35 +377,35 @@
44.397 val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
44.398
44.399 val _ =
44.400 - Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
44.401 - (Keyword.tag_ml Keyword.thy_decl)
44.402 + Outer_Syntax.command ("parse_ast_translation", Keyword.tag_ml Keyword.thy_decl)
44.403 + "install parse ast translation functions"
44.404 (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
44.405
44.406 val _ =
44.407 - Outer_Syntax.command "parse_translation" "install parse translation functions"
44.408 - (Keyword.tag_ml Keyword.thy_decl)
44.409 + Outer_Syntax.command ("parse_translation", Keyword.tag_ml Keyword.thy_decl)
44.410 + "install parse translation functions"
44.411 (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
44.412
44.413 val _ =
44.414 - Outer_Syntax.command "print_translation" "install print translation functions"
44.415 - (Keyword.tag_ml Keyword.thy_decl)
44.416 + Outer_Syntax.command ("print_translation", Keyword.tag_ml Keyword.thy_decl)
44.417 + "install print translation functions"
44.418 (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
44.419
44.420 val _ =
44.421 - Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
44.422 - (Keyword.tag_ml Keyword.thy_decl)
44.423 + Outer_Syntax.command ("typed_print_translation", Keyword.tag_ml Keyword.thy_decl)
44.424 + "install typed print translation functions"
44.425 (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
44.426
44.427 val _ =
44.428 - Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
44.429 - (Keyword.tag_ml Keyword.thy_decl)
44.430 + Outer_Syntax.command ("print_ast_translation", Keyword.tag_ml Keyword.thy_decl)
44.431 + "install print ast translation functions"
44.432 (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
44.433
44.434
44.435 (* oracles *)
44.436
44.437 val _ =
44.438 - Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
44.439 + Outer_Syntax.command ("oracle", Keyword.tag_ml Keyword.thy_decl) "declare oracle"
44.440 (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
44.441 (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
44.442
44.443 @@ -389,7 +413,7 @@
44.444 (* local theories *)
44.445
44.446 val _ =
44.447 - Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
44.448 + Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
44.449 (Parse.position Parse.name --| Parse.begin >> (fn name =>
44.450 Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
44.451
44.452 @@ -402,7 +426,7 @@
44.453 Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
44.454
44.455 val _ =
44.456 - Outer_Syntax.command "locale" "define named proof context" Keyword.thy_decl
44.457 + Outer_Syntax.command ("locale", Keyword.thy_decl) "define named proof context"
44.458 (Parse.binding --
44.459 Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
44.460 >> (fn ((name, (expr, elems)), begin) =>
44.461 @@ -415,24 +439,23 @@
44.462 (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
44.463
44.464 val _ =
44.465 - Outer_Syntax.command "sublocale"
44.466 - "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
44.467 + Outer_Syntax.command ("sublocale", Keyword.thy_goal)
44.468 + "prove sublocale relation between a locale and a locale expression"
44.469 (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
44.470 parse_interpretation_arguments false
44.471 >> (fn (loc, (expr, equations)) =>
44.472 Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
44.473
44.474 val _ =
44.475 - Outer_Syntax.command "interpretation"
44.476 - "prove interpretation of locale expression in theory" Keyword.thy_goal
44.477 + Outer_Syntax.command ("interpretation", Keyword.thy_goal)
44.478 + "prove interpretation of locale expression in theory"
44.479 (parse_interpretation_arguments true
44.480 >> (fn (expr, equations) => Toplevel.print o
44.481 Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
44.482
44.483 val _ =
44.484 - Outer_Syntax.command "interpret"
44.485 + Outer_Syntax.command ("interpret", Keyword.tag_proof Keyword.prf_goal)
44.486 "prove interpretation of locale expression in proof context"
44.487 - (Keyword.tag_proof Keyword.prf_goal)
44.488 (parse_interpretation_arguments true
44.489 >> (fn (expr, equations) => Toplevel.print o
44.490 Toplevel.proof' (Expression.interpret_cmd expr equations)));
44.491 @@ -446,24 +469,24 @@
44.492 Scan.repeat1 Parse_Spec.context_element >> pair [];
44.493
44.494 val _ =
44.495 - Outer_Syntax.command "class" "define type class" Keyword.thy_decl
44.496 + Outer_Syntax.command ("class", Keyword.thy_decl) "define type class"
44.497 (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
44.498 >> (fn ((name, (supclasses, elems)), begin) =>
44.499 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
44.500 (Class_Declaration.class_cmd I name supclasses elems #> snd)));
44.501
44.502 val _ =
44.503 - Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
44.504 + Outer_Syntax.local_theory_to_proof ("subclass", Keyword.thy_goal) "prove a subclass relation"
44.505 (Parse.class >> Class_Declaration.subclass_cmd I);
44.506
44.507 val _ =
44.508 - Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
44.509 + Outer_Syntax.command ("instantiation", Keyword.thy_decl) "instantiate and prove type arity"
44.510 (Parse.multi_arity --| Parse.begin
44.511 >> (fn arities => Toplevel.print o
44.512 Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
44.513
44.514 val _ =
44.515 - Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
44.516 + Outer_Syntax.command ("instance", Keyword.thy_goal) "prove type arity or subclass relation"
44.517 ((Parse.class --
44.518 ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
44.519 Parse.multi_arity >> Class.instance_arity_cmd)
44.520 @@ -475,7 +498,7 @@
44.521 (* arbitrary overloading *)
44.522
44.523 val _ =
44.524 - Outer_Syntax.command "overloading" "overloaded definitions" Keyword.thy_decl
44.525 + Outer_Syntax.command ("overloading", Keyword.thy_decl) "overloaded definitions"
44.526 (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
44.527 Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
44.528 >> Parse.triple1) --| Parse.begin
44.529 @@ -486,7 +509,8 @@
44.530 (* code generation *)
44.531
44.532 val _ =
44.533 - Outer_Syntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
44.534 + Outer_Syntax.command ("code_datatype", Keyword.thy_decl)
44.535 + "define set of code datatype constructors"
44.536 (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
44.537
44.538
44.539 @@ -497,9 +521,9 @@
44.540
44.541 fun gen_theorem schematic kind =
44.542 Outer_Syntax.local_theory_to_proof'
44.543 - (if schematic then "schematic_" ^ kind else kind)
44.544 + (if schematic then ("schematic_" ^ kind, Keyword.thy_schematic_goal)
44.545 + else (kind, Keyword.thy_goal))
44.546 ("state " ^ (if schematic then "schematic " ^ kind else kind))
44.547 - (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
44.548 (Scan.optional (Parse_Spec.opt_thm_name ":" --|
44.549 Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
44.550 Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
44.551 @@ -514,28 +538,25 @@
44.552 val _ = gen_theorem true Thm.corollaryK;
44.553
44.554 val _ =
44.555 - Outer_Syntax.local_theory_to_proof "notepad"
44.556 - "Isar proof state as formal notepad, without any result" Keyword.thy_decl
44.557 + Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
44.558 + "Isar proof state as formal notepad, without any result"
44.559 (Parse.begin >> K Proof.begin_notepad);
44.560
44.561 val _ =
44.562 - Outer_Syntax.command "have" "state local goal"
44.563 - (Keyword.tag_proof Keyword.prf_goal)
44.564 + Outer_Syntax.command ("have", Keyword.tag_proof Keyword.prf_goal) "state local goal"
44.565 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
44.566
44.567 val _ =
44.568 - Outer_Syntax.command "hence" "abbreviates \"then have\""
44.569 - (Keyword.tag_proof Keyword.prf_goal)
44.570 + Outer_Syntax.command ("hence", Keyword.tag_proof Keyword.prf_goal) "abbreviates \"then have\""
44.571 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
44.572
44.573 val _ =
44.574 - Outer_Syntax.command "show" "state local goal, solving current obligation"
44.575 - (Keyword.tag_proof Keyword.prf_asm_goal)
44.576 + Outer_Syntax.command ("show", Keyword.tag_proof Keyword.prf_asm_goal)
44.577 + "state local goal, solving current obligation"
44.578 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
44.579
44.580 val _ =
44.581 - Outer_Syntax.command "thus" "abbreviates \"then show\""
44.582 - (Keyword.tag_proof Keyword.prf_asm_goal)
44.583 + Outer_Syntax.command ("thus", Keyword.tag_proof Keyword.prf_asm_goal) "abbreviates \"then show\""
44.584 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
44.585
44.586
44.587 @@ -544,56 +565,51 @@
44.588 val facts = Parse.and_list1 Parse_Spec.xthms1;
44.589
44.590 val _ =
44.591 - Outer_Syntax.command "then" "forward chaining"
44.592 - (Keyword.tag_proof Keyword.prf_chain)
44.593 + Outer_Syntax.command ("then", Keyword.tag_proof Keyword.prf_chain) "forward chaining"
44.594 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
44.595
44.596 val _ =
44.597 - Outer_Syntax.command "from" "forward chaining from given facts"
44.598 - (Keyword.tag_proof Keyword.prf_chain)
44.599 + Outer_Syntax.command ("from", Keyword.tag_proof Keyword.prf_chain)
44.600 + "forward chaining from given facts"
44.601 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
44.602
44.603 val _ =
44.604 - Outer_Syntax.command "with" "forward chaining from given and current facts"
44.605 - (Keyword.tag_proof Keyword.prf_chain)
44.606 + Outer_Syntax.command ("with", Keyword.tag_proof Keyword.prf_chain)
44.607 + "forward chaining from given and current facts"
44.608 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
44.609
44.610 val _ =
44.611 - Outer_Syntax.command "note" "define facts"
44.612 - (Keyword.tag_proof Keyword.prf_decl)
44.613 + Outer_Syntax.command ("note", Keyword.tag_proof Keyword.prf_decl) "define facts"
44.614 (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
44.615
44.616 val _ =
44.617 - Outer_Syntax.command "using" "augment goal facts"
44.618 - (Keyword.tag_proof Keyword.prf_decl)
44.619 + Outer_Syntax.command ("using", Keyword.tag_proof Keyword.prf_decl) "augment goal facts"
44.620 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
44.621
44.622 val _ =
44.623 - Outer_Syntax.command "unfolding" "unfold definitions in goal and facts"
44.624 - (Keyword.tag_proof Keyword.prf_decl)
44.625 + Outer_Syntax.command ("unfolding", Keyword.tag_proof Keyword.prf_decl)
44.626 + "unfold definitions in goal and facts"
44.627 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
44.628
44.629
44.630 (* proof context *)
44.631
44.632 val _ =
44.633 - Outer_Syntax.command "fix" "fix local variables (Skolem constants)"
44.634 - (Keyword.tag_proof Keyword.prf_asm)
44.635 + Outer_Syntax.command ("fix", Keyword.tag_proof Keyword.prf_asm)
44.636 + "fix local variables (Skolem constants)"
44.637 (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
44.638
44.639 val _ =
44.640 - Outer_Syntax.command "assume" "assume propositions"
44.641 - (Keyword.tag_proof Keyword.prf_asm)
44.642 + Outer_Syntax.command ("assume", Keyword.tag_proof Keyword.prf_asm) "assume propositions"
44.643 (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
44.644
44.645 val _ =
44.646 - Outer_Syntax.command "presume" "assume propositions, to be established later"
44.647 - (Keyword.tag_proof Keyword.prf_asm)
44.648 + Outer_Syntax.command ("presume", Keyword.tag_proof Keyword.prf_asm)
44.649 + "assume propositions, to be established later"
44.650 (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
44.651
44.652 val _ =
44.653 - Outer_Syntax.command "def" "local definition"
44.654 - (Keyword.tag_proof Keyword.prf_asm)
44.655 + Outer_Syntax.command ("def", Keyword.tag_proof Keyword.prf_asm) "local definition"
44.656 (Parse.and_list1
44.657 (Parse_Spec.opt_thm_name ":" --
44.658 ((Parse.binding -- Parse.opt_mixfix) --
44.659 @@ -601,25 +617,24 @@
44.660 >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
44.661
44.662 val _ =
44.663 - Outer_Syntax.command "obtain" "generalized existence"
44.664 - (Keyword.tag_proof Keyword.prf_asm_goal)
44.665 + Outer_Syntax.command ("obtain", Keyword.tag_proof Keyword.prf_asm_goal)
44.666 + "generalized elimination"
44.667 (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
44.668 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
44.669
44.670 val _ =
44.671 - Outer_Syntax.command "guess" "wild guessing (unstructured)"
44.672 - (Keyword.tag_proof Keyword.prf_asm_goal)
44.673 + Outer_Syntax.command ("guess", Keyword.tag_proof Keyword.prf_asm_goal)
44.674 + "wild guessing (unstructured)"
44.675 (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
44.676
44.677 val _ =
44.678 - Outer_Syntax.command "let" "bind text variables"
44.679 - (Keyword.tag_proof Keyword.prf_decl)
44.680 + Outer_Syntax.command ("let", Keyword.tag_proof Keyword.prf_decl) "bind text variables"
44.681 (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
44.682 >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
44.683
44.684 val _ =
44.685 - Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
44.686 - (Keyword.tag_proof Keyword.prf_decl)
44.687 + Outer_Syntax.command ("write", Keyword.tag_proof Keyword.prf_decl)
44.688 + "add concrete syntax for constants / fixed variables"
44.689 (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
44.690 >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
44.691
44.692 @@ -629,92 +644,81 @@
44.693 Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
44.694
44.695 val _ =
44.696 - Outer_Syntax.command "case" "invoke local context"
44.697 - (Keyword.tag_proof Keyword.prf_asm)
44.698 + Outer_Syntax.command ("case", Keyword.tag_proof Keyword.prf_asm) "invoke local context"
44.699 (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
44.700
44.701
44.702 (* proof structure *)
44.703
44.704 val _ =
44.705 - Outer_Syntax.command "{" "begin explicit proof block"
44.706 - (Keyword.tag_proof Keyword.prf_open)
44.707 + Outer_Syntax.command ("{", Keyword.tag_proof Keyword.prf_open) "begin explicit proof block"
44.708 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
44.709
44.710 val _ =
44.711 - Outer_Syntax.command "}" "end explicit proof block"
44.712 - (Keyword.tag_proof Keyword.prf_close)
44.713 + Outer_Syntax.command ("}", Keyword.tag_proof Keyword.prf_close) "end explicit proof block"
44.714 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
44.715
44.716 val _ =
44.717 - Outer_Syntax.command "next" "enter next proof block"
44.718 - (Keyword.tag_proof Keyword.prf_block)
44.719 + Outer_Syntax.command ("next", Keyword.tag_proof Keyword.prf_block) "enter next proof block"
44.720 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
44.721
44.722
44.723 (* end proof *)
44.724
44.725 val _ =
44.726 - Outer_Syntax.command "qed" "conclude (sub-)proof"
44.727 - (Keyword.tag_proof Keyword.qed_block)
44.728 + Outer_Syntax.command ("qed", Keyword.tag_proof Keyword.qed_block) "conclude (sub-)proof"
44.729 (Scan.option Method.parse >> Isar_Cmd.qed);
44.730
44.731 val _ =
44.732 - Outer_Syntax.command "by" "terminal backward proof"
44.733 - (Keyword.tag_proof Keyword.qed)
44.734 + Outer_Syntax.command ("by", Keyword.tag_proof Keyword.qed) "terminal backward proof"
44.735 (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
44.736
44.737 val _ =
44.738 - Outer_Syntax.command ".." "default proof"
44.739 - (Keyword.tag_proof Keyword.qed)
44.740 + Outer_Syntax.command ("..", Keyword.tag_proof Keyword.qed) "default proof"
44.741 (Scan.succeed Isar_Cmd.default_proof);
44.742
44.743 val _ =
44.744 - Outer_Syntax.command "." "immediate proof"
44.745 - (Keyword.tag_proof Keyword.qed)
44.746 + Outer_Syntax.command (".", Keyword.tag_proof Keyword.qed) "immediate proof"
44.747 (Scan.succeed Isar_Cmd.immediate_proof);
44.748
44.749 val _ =
44.750 - Outer_Syntax.command "done" "done proof"
44.751 - (Keyword.tag_proof Keyword.qed)
44.752 + Outer_Syntax.command ("done", Keyword.tag_proof Keyword.qed) "done proof"
44.753 (Scan.succeed Isar_Cmd.done_proof);
44.754
44.755 val _ =
44.756 - Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
44.757 - (Keyword.tag_proof Keyword.qed)
44.758 + Outer_Syntax.command ("sorry", Keyword.tag_proof Keyword.qed)
44.759 + "skip proof (quick-and-dirty mode only!)"
44.760 (Scan.succeed Isar_Cmd.skip_proof);
44.761
44.762 val _ =
44.763 - Outer_Syntax.command "oops" "forget proof"
44.764 - (Keyword.tag_proof Keyword.qed_global)
44.765 + Outer_Syntax.command ("oops", Keyword.tag_proof Keyword.qed_global) "forget proof"
44.766 (Scan.succeed Toplevel.forget_proof);
44.767
44.768
44.769 (* proof steps *)
44.770
44.771 val _ =
44.772 - Outer_Syntax.command "defer" "shuffle internal proof state"
44.773 - (Keyword.tag_proof Keyword.prf_script)
44.774 + Outer_Syntax.command ("defer", Keyword.tag_proof Keyword.prf_script)
44.775 + "shuffle internal proof state"
44.776 (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
44.777
44.778 val _ =
44.779 - Outer_Syntax.command "prefer" "shuffle internal proof state"
44.780 - (Keyword.tag_proof Keyword.prf_script)
44.781 + Outer_Syntax.command ("prefer", Keyword.tag_proof Keyword.prf_script)
44.782 + "shuffle internal proof state"
44.783 (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
44.784
44.785 val _ =
44.786 - Outer_Syntax.command "apply" "initial refinement step (unstructured)"
44.787 - (Keyword.tag_proof Keyword.prf_script)
44.788 + Outer_Syntax.command ("apply", Keyword.tag_proof Keyword.prf_script)
44.789 + "initial refinement step (unstructured)"
44.790 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
44.791
44.792 val _ =
44.793 - Outer_Syntax.command "apply_end" "terminal refinement (unstructured)"
44.794 - (Keyword.tag_proof Keyword.prf_script)
44.795 + Outer_Syntax.command ("apply_end", Keyword.tag_proof Keyword.prf_script)
44.796 + "terminal refinement (unstructured)"
44.797 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
44.798
44.799 val _ =
44.800 - Outer_Syntax.command "proof" "backward proof"
44.801 - (Keyword.tag_proof Keyword.prf_block)
44.802 + Outer_Syntax.command ("proof", Keyword.tag_proof Keyword.prf_block) "backward proof"
44.803 (Scan.option Method.parse >> (fn m => Toplevel.print o
44.804 Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
44.805 Toplevel.skip_proof (fn i => i + 1)));
44.806 @@ -726,31 +730,31 @@
44.807 Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
44.808
44.809 val _ =
44.810 - Outer_Syntax.command "also" "combine calculation and current facts"
44.811 - (Keyword.tag_proof Keyword.prf_decl)
44.812 + Outer_Syntax.command ("also", Keyword.tag_proof Keyword.prf_decl)
44.813 + "combine calculation and current facts"
44.814 (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
44.815
44.816 val _ =
44.817 - Outer_Syntax.command "finally" "combine calculation and current facts, exhibit result"
44.818 - (Keyword.tag_proof Keyword.prf_chain)
44.819 + Outer_Syntax.command ("finally", Keyword.tag_proof Keyword.prf_chain)
44.820 + "combine calculation and current facts, exhibit result"
44.821 (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
44.822
44.823 val _ =
44.824 - Outer_Syntax.command "moreover" "augment calculation by current facts"
44.825 - (Keyword.tag_proof Keyword.prf_decl)
44.826 + Outer_Syntax.command ("moreover", Keyword.tag_proof Keyword.prf_decl)
44.827 + "augment calculation by current facts"
44.828 (Scan.succeed (Toplevel.proof' Calculation.moreover));
44.829
44.830 val _ =
44.831 - Outer_Syntax.command "ultimately" "augment calculation by current facts, exhibit result"
44.832 - (Keyword.tag_proof Keyword.prf_chain)
44.833 + Outer_Syntax.command ("ultimately", Keyword.tag_proof Keyword.prf_chain)
44.834 + "augment calculation by current facts, exhibit result"
44.835 (Scan.succeed (Toplevel.proof' Calculation.ultimately));
44.836
44.837
44.838 (* proof navigation *)
44.839
44.840 val _ =
44.841 - Outer_Syntax.command "back" "backtracking of proof command"
44.842 - (Keyword.tag_proof Keyword.prf_script)
44.843 + Outer_Syntax.command ("back", Keyword.tag_proof Keyword.prf_script)
44.844 + "backtracking of proof command"
44.845 (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
44.846
44.847
44.848 @@ -762,7 +766,7 @@
44.849 (Position.of_properties (Position.default_properties pos props), str));
44.850
44.851 val _ =
44.852 - Outer_Syntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
44.853 + Outer_Syntax.improper_command ("Isabelle.command", Keyword.control) "nested Isabelle command"
44.854 (props_text :|-- (fn (pos, str) =>
44.855 (case Outer_Syntax.parse pos str of
44.856 [tr] => Scan.succeed (K tr)
44.857 @@ -779,152 +783,161 @@
44.858 val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
44.859
44.860 val _ =
44.861 - Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
44.862 - Keyword.diag (Parse.nat >>
44.863 + Outer_Syntax.improper_command ("pretty_setmargin", Keyword.diag)
44.864 + "change default margin for pretty printing"
44.865 + (Parse.nat >>
44.866 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
44.867
44.868 val _ =
44.869 - Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
44.870 + Outer_Syntax.improper_command ("help", Keyword.diag) "print outer syntax commands"
44.871 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
44.872
44.873 val _ =
44.874 - Outer_Syntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
44.875 + Outer_Syntax.improper_command ("print_commands", Keyword.diag) "print outer syntax commands"
44.876 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
44.877
44.878 val _ =
44.879 - Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
44.880 + Outer_Syntax.improper_command ("print_configs", Keyword.diag) "print configuration options"
44.881 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
44.882
44.883 val _ =
44.884 - Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
44.885 + Outer_Syntax.improper_command ("print_context", Keyword.diag) "print theory context name"
44.886 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
44.887
44.888 val _ =
44.889 - Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
44.890 - Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
44.891 + Outer_Syntax.improper_command ("print_theory", Keyword.diag)
44.892 + "print logical theory contents (verbose!)"
44.893 + (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
44.894
44.895 val _ =
44.896 - Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
44.897 - Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
44.898 + Outer_Syntax.improper_command ("print_syntax", Keyword.diag)
44.899 + "print inner syntax of context (verbose!)"
44.900 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
44.901
44.902 val _ =
44.903 - Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
44.904 - Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
44.905 + Outer_Syntax.improper_command ("print_abbrevs", Keyword.diag)
44.906 + "print constant abbreviation of context"
44.907 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
44.908
44.909 val _ =
44.910 - Outer_Syntax.improper_command "print_theorems"
44.911 - "print theorems of local theory or proof context" Keyword.diag
44.912 + Outer_Syntax.improper_command ("print_theorems", Keyword.diag)
44.913 + "print theorems of local theory or proof context"
44.914 (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
44.915
44.916 val _ =
44.917 - Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
44.918 + Outer_Syntax.improper_command ("print_locales", Keyword.diag)
44.919 + "print locales of this theory"
44.920 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
44.921
44.922 val _ =
44.923 - Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
44.924 + Outer_Syntax.improper_command ("print_classes", Keyword.diag) "print classes of this theory"
44.925 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
44.926 Toplevel.keep (Class.print_classes o Toplevel.context_of)));
44.927
44.928 val _ =
44.929 - Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
44.930 + Outer_Syntax.improper_command ("print_locale", Keyword.diag) "print locale of this theory"
44.931 (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
44.932
44.933 val _ =
44.934 - Outer_Syntax.improper_command "print_interps"
44.935 - "print interpretations of locale for this theory or proof context" Keyword.diag
44.936 + Outer_Syntax.improper_command ("print_interps", Keyword.diag)
44.937 + "print interpretations of locale for this theory or proof context"
44.938 (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
44.939
44.940 val _ =
44.941 - Outer_Syntax.improper_command "print_dependencies"
44.942 - "print dependencies of locale expression" Keyword.diag
44.943 + Outer_Syntax.improper_command ("print_dependencies", Keyword.diag)
44.944 + "print dependencies of locale expression"
44.945 (opt_bang -- Parse_Spec.locale_expression true >>
44.946 (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
44.947
44.948 val _ =
44.949 - Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
44.950 + Outer_Syntax.improper_command ("print_attributes", Keyword.diag)
44.951 + "print attributes of this theory"
44.952 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
44.953
44.954 val _ =
44.955 - Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
44.956 + Outer_Syntax.improper_command ("print_simpset", Keyword.diag)
44.957 + "print context of Simplifier"
44.958 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
44.959
44.960 val _ =
44.961 - Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
44.962 + Outer_Syntax.improper_command ("print_rules", Keyword.diag) "print intro/elim rules"
44.963 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
44.964
44.965 val _ =
44.966 - Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
44.967 + Outer_Syntax.improper_command ("print_trans_rules", Keyword.diag) "print transitivity rules"
44.968 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
44.969
44.970 val _ =
44.971 - Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
44.972 + Outer_Syntax.improper_command ("print_methods", Keyword.diag) "print methods of this theory"
44.973 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
44.974
44.975 val _ =
44.976 - Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
44.977 + Outer_Syntax.improper_command ("print_antiquotations", Keyword.diag)
44.978 + "print antiquotations (global)"
44.979 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
44.980
44.981 val _ =
44.982 - Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
44.983 - Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
44.984 + Outer_Syntax.improper_command ("thy_deps", Keyword.diag) "visualize theory dependencies"
44.985 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
44.986
44.987 val _ =
44.988 - Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
44.989 - Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
44.990 + Outer_Syntax.improper_command ("class_deps", Keyword.diag) "visualize class dependencies"
44.991 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
44.992
44.993 val _ =
44.994 - Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
44.995 - Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
44.996 + Outer_Syntax.improper_command ("thm_deps", Keyword.diag) "visualize theorem dependencies"
44.997 + (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
44.998
44.999 val _ =
44.1000 - Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
44.1001 + Outer_Syntax.improper_command ("print_binds", Keyword.diag) "print term bindings of proof context"
44.1002 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
44.1003
44.1004 val _ =
44.1005 - Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
44.1006 + Outer_Syntax.improper_command ("print_facts", Keyword.diag) "print facts of proof context"
44.1007 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
44.1008
44.1009 val _ =
44.1010 - Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
44.1011 + Outer_Syntax.improper_command ("print_cases", Keyword.diag) "print cases of proof context"
44.1012 (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
44.1013
44.1014 val _ =
44.1015 - Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
44.1016 + Outer_Syntax.improper_command ("print_statement", Keyword.diag)
44.1017 + "print theorems as long statements"
44.1018 (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
44.1019
44.1020 val _ =
44.1021 - Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
44.1022 + Outer_Syntax.improper_command ("thm", Keyword.diag) "print theorems"
44.1023 (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
44.1024
44.1025 val _ =
44.1026 - Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
44.1027 + Outer_Syntax.improper_command ("prf", Keyword.diag) "print proof terms of theorems"
44.1028 (opt_modes -- Scan.option Parse_Spec.xthms1
44.1029 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
44.1030
44.1031 val _ =
44.1032 - Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
44.1033 + Outer_Syntax.improper_command ("full_prf", Keyword.diag) "print full proof terms of theorems"
44.1034 (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
44.1035
44.1036 val _ =
44.1037 - Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
44.1038 + Outer_Syntax.improper_command ("prop", Keyword.diag) "read and print proposition"
44.1039 (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
44.1040
44.1041 val _ =
44.1042 - Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
44.1043 + Outer_Syntax.improper_command ("term", Keyword.diag) "read and print term"
44.1044 (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
44.1045
44.1046 val _ =
44.1047 - Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
44.1048 + Outer_Syntax.improper_command ("typ", Keyword.diag) "read and print type"
44.1049 (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
44.1050
44.1051 val _ =
44.1052 - Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
44.1053 + Outer_Syntax.improper_command ("print_codesetup", Keyword.diag) "print code generator setup"
44.1054 (Scan.succeed
44.1055 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
44.1056 (Code.print_codesetup o Toplevel.theory_of)));
44.1057
44.1058 val _ =
44.1059 - Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
44.1060 + Outer_Syntax.improper_command ("unused_thms", Keyword.diag) "find unused theorems"
44.1061 (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
44.1062 Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
44.1063 (Toplevel.no_timing oo Isar_Cmd.unused_thms));
44.1064 @@ -934,39 +947,42 @@
44.1065 (** system commands (for interactive mode only) **)
44.1066
44.1067 val _ =
44.1068 - Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control
44.1069 + Outer_Syntax.improper_command ("cd", Keyword.control) "change current working directory"
44.1070 (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
44.1071
44.1072 val _ =
44.1073 - Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
44.1074 + Outer_Syntax.improper_command ("pwd", Keyword.diag) "print current working directory"
44.1075 (Scan.succeed (Toplevel.no_timing o
44.1076 Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
44.1077
44.1078 val _ =
44.1079 - Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
44.1080 + Outer_Syntax.improper_command ("use_thy", Keyword.control) "use theory file"
44.1081 (Parse.name >> (fn name =>
44.1082 Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
44.1083
44.1084 val _ =
44.1085 - Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
44.1086 + Outer_Syntax.improper_command ("remove_thy", Keyword.control) "remove theory from loader database"
44.1087 (Parse.name >> (fn name =>
44.1088 Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
44.1089
44.1090 val _ =
44.1091 - Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
44.1092 - Keyword.control (Parse.name >> (fn name =>
44.1093 + Outer_Syntax.improper_command ("kill_thy", Keyword.control)
44.1094 + "kill theory -- try to remove from loader database"
44.1095 + (Parse.name >> (fn name =>
44.1096 Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
44.1097
44.1098 val _ =
44.1099 - Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
44.1100 - Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
44.1101 + Outer_Syntax.improper_command ("display_drafts", Keyword.diag)
44.1102 + "display raw source files with symbols"
44.1103 + (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
44.1104
44.1105 val _ =
44.1106 - Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
44.1107 - Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
44.1108 + Outer_Syntax.improper_command ("print_drafts", Keyword.diag)
44.1109 + "print raw source files with symbols"
44.1110 + (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
44.1111
44.1112 val _ = (* FIXME tty only *)
44.1113 - Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
44.1114 + Outer_Syntax.improper_command ("pr", Keyword.diag) "print current proof state (if present)"
44.1115 (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
44.1116 Toplevel.no_timing o Toplevel.keep (fn state =>
44.1117 (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
44.1118 @@ -974,23 +990,26 @@
44.1119 Print_Mode.with_modes modes (Toplevel.print_state true) state))));
44.1120
44.1121 val _ =
44.1122 - Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
44.1123 + Outer_Syntax.improper_command ("disable_pr", Keyword.control)
44.1124 + "disable printing of toplevel state"
44.1125 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
44.1126
44.1127 val _ =
44.1128 - Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
44.1129 + Outer_Syntax.improper_command ("enable_pr", Keyword.control)
44.1130 + "enable printing of toplevel state"
44.1131 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
44.1132
44.1133 val _ =
44.1134 - Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control
44.1135 + Outer_Syntax.improper_command ("commit", Keyword.control)
44.1136 + "commit current session to ML database"
44.1137 (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
44.1138
44.1139 val _ =
44.1140 - Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
44.1141 + Outer_Syntax.improper_command ("quit", Keyword.control) "quit Isabelle"
44.1142 (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
44.1143
44.1144 val _ =
44.1145 - Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
44.1146 + Outer_Syntax.improper_command ("exit", Keyword.control) "exit Isar loop"
44.1147 (Scan.succeed
44.1148 (Toplevel.no_timing o Toplevel.keep (fn state =>
44.1149 (Context.set_thread_data (try Toplevel.generic_theory_of state);
45.1 --- a/src/Pure/Isar/keyword.ML Fri Mar 16 16:32:34 2012 +0000
45.2 +++ b/src/Pure/Isar/keyword.ML Fri Mar 16 18:21:22 2012 +0100
45.3 @@ -37,7 +37,9 @@
45.4 val tag_theory: T -> T
45.5 val tag_proof: T -> T
45.6 val tag_ml: T -> T
45.7 - val make: string * string list -> T
45.8 + type spec = string * string list
45.9 + val spec: spec -> T
45.10 + val command_spec: string * spec -> string * T
45.11 val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
45.12 val is_keyword: string -> bool
45.13 val command_keyword: string -> T option
45.14 @@ -65,7 +67,7 @@
45.15
45.16 (** keyword classification **)
45.17
45.18 -datatype T = Keyword of string * string list;
45.19 +datatype T = Keyword of string * string list; (*kind, tags (in canonical reverse order)*)
45.20
45.21 fun kind s = Keyword (s, []);
45.22 fun kind_of (Keyword (s, _)) = s;
45.23 @@ -141,11 +143,15 @@
45.24 ("prf_asm_goal", prf_asm_goal),
45.25 ("prf_script", prf_script)];
45.26
45.27 -fun make (kind, tags) =
45.28 +type spec = string * string list;
45.29 +
45.30 +fun spec (kind, tags) =
45.31 (case Symtab.lookup name_table kind of
45.32 SOME k => k |> fold tag tags
45.33 | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
45.34
45.35 +fun command_spec (name, s) = (name, spec s);
45.36 +
45.37
45.38
45.39 (** global keyword tables **)
46.1 --- a/src/Pure/Isar/outer_syntax.ML Fri Mar 16 16:32:34 2012 +0000
46.2 +++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 16 18:21:22 2012 +0100
46.3 @@ -12,21 +12,20 @@
46.4 type outer_syntax
46.5 val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
46.6 val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
46.7 - val command: string -> string -> Keyword.T ->
46.8 + type command_spec = string * Keyword.T
46.9 + val command: command_spec -> string ->
46.10 (Toplevel.transition -> Toplevel.transition) parser -> unit
46.11 - val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
46.12 + val markup_command: Thy_Output.markup -> command_spec -> string ->
46.13 (Toplevel.transition -> Toplevel.transition) parser -> unit
46.14 - val improper_command: string -> string -> Keyword.T ->
46.15 + val improper_command: command_spec -> string ->
46.16 (Toplevel.transition -> Toplevel.transition) parser -> unit
46.17 - val internal_command: string ->
46.18 - (Toplevel.transition -> Toplevel.transition) parser -> unit
46.19 - val local_theory': string -> string -> Keyword.T ->
46.20 + val local_theory': command_spec -> string ->
46.21 (bool -> local_theory -> local_theory) parser -> unit
46.22 - val local_theory: string -> string -> Keyword.T ->
46.23 + val local_theory: command_spec -> string ->
46.24 (local_theory -> local_theory) parser -> unit
46.25 - val local_theory_to_proof': string -> string -> Keyword.T ->
46.26 + val local_theory_to_proof': command_spec -> string ->
46.27 (bool -> local_theory -> Proof.state) parser -> unit
46.28 - val local_theory_to_proof: string -> string -> Keyword.T ->
46.29 + val local_theory_to_proof: command_spec -> string ->
46.30 (local_theory -> Proof.state) parser -> unit
46.31 val print_outer_syntax: unit -> unit
46.32 val scan: Position.T -> string -> Token.T list
46.33 @@ -117,21 +116,24 @@
46.34
46.35 (** global outer syntax **)
46.36
46.37 +type command_spec = string * Keyword.T;
46.38 +
46.39 local
46.40
46.41 (*synchronized wrt. Keywords*)
46.42 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
46.43
46.44 -fun add_command name kind cmd = CRITICAL (fn () =>
46.45 +fun add_command (name, kind) cmd = CRITICAL (fn () =>
46.46 let
46.47 val thy = ML_Context.the_global_context ();
46.48 val _ =
46.49 (case try (Thy_Header.the_keyword thy) name of
46.50 - SOME k =>
46.51 - if k = SOME kind then ()
46.52 + SOME spec =>
46.53 + if Option.map Keyword.spec spec = SOME kind then ()
46.54 else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
46.55 | NONE =>
46.56 - if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
46.57 + if Context.theory_name thy = Context.PureN
46.58 + then Keyword.define (name, SOME kind)
46.59 else error ("Undeclared outer syntax command " ^ quote name));
46.60 in
46.61 Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
46.62 @@ -146,25 +148,22 @@
46.63
46.64 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
46.65
46.66 -fun command name comment kind parse =
46.67 - add_command name kind (make_command comment NONE false parse);
46.68 +fun command command_spec comment parse =
46.69 + add_command command_spec (make_command comment NONE false parse);
46.70
46.71 -fun markup_command markup name comment kind parse =
46.72 - add_command name kind (make_command comment (SOME markup) false parse);
46.73 +fun markup_command markup command_spec comment parse =
46.74 + add_command command_spec (make_command comment (SOME markup) false parse);
46.75
46.76 -fun improper_command name comment kind parse =
46.77 - add_command name kind (make_command comment NONE true parse);
46.78 -
46.79 -fun internal_command name parse =
46.80 - command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
46.81 +fun improper_command command_spec comment parse =
46.82 + add_command command_spec (make_command comment NONE true parse);
46.83
46.84 end;
46.85
46.86
46.87 (* local_theory commands *)
46.88
46.89 -fun local_theory_command do_print trans name comment kind parse =
46.90 - command name comment kind (Parse.opt_target -- parse
46.91 +fun local_theory_command do_print trans command_spec comment parse =
46.92 + command command_spec comment (Parse.opt_target -- parse
46.93 >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
46.94
46.95 val local_theory' = local_theory_command false Toplevel.local_theory';
47.1 --- a/src/Pure/ML/ml_antiquote.ML Fri Mar 16 16:32:34 2012 +0000
47.2 +++ b/src/Pure/ML/ml_antiquote.ML Fri Mar 16 18:21:22 2012 +0100
47.3 @@ -66,8 +66,7 @@
47.4 inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
47.5
47.6 value (Binding.name "binding")
47.7 - (Scan.lift (Parse.position Args.name)
47.8 - >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
47.9 + (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
47.10
47.11 value (Binding.name "theory")
47.12 (Scan.lift Args.name >> (fn name =>
47.13 @@ -97,10 +96,10 @@
47.14 "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
47.15
47.16 value (Binding.name "cterm") (Args.term >> (fn t =>
47.17 - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
47.18 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
47.19
47.20 value (Binding.name "cprop") (Args.prop >> (fn t =>
47.21 - "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
47.22 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
47.23
47.24 value (Binding.name "cpat")
47.25 (Args.context --
47.26 @@ -185,13 +184,24 @@
47.27
47.28 (* outer syntax *)
47.29
47.30 +fun with_keyword f =
47.31 + Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
47.32 + (f (name, Thy_Header.the_keyword thy name)
47.33 + handle ERROR msg => error (msg ^ Position.str_of pos)));
47.34 +
47.35 val _ = Context.>> (Context.map_theory
47.36 - (value (Binding.name "keyword")
47.37 - (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
47.38 - (if is_none (Thy_Header.the_keyword thy name) then
47.39 - ML_Syntax.atomic ("Parse.$$$ " ^ ML_Syntax.print_string name)
47.40 - else error ("Unknown minor keyword " ^ quote name))
47.41 - handle ERROR msg => error (msg ^ Position.str_of pos)))));
47.42 + (value (Binding.name "keyword")
47.43 + (with_keyword
47.44 + (fn (name, NONE) => "Parse.$$$ " ^ ML_Syntax.print_string name
47.45 + | (name, SOME _) => error ("Expected minor keyword " ^ quote name))) #>
47.46 + value (Binding.name "command_spec")
47.47 + (with_keyword
47.48 + (fn (name, SOME kind) =>
47.49 + "Keyword.command_spec " ^ ML_Syntax.atomic
47.50 + (ML_Syntax.print_pair ML_Syntax.print_string
47.51 + (ML_Syntax.print_pair ML_Syntax.print_string
47.52 + (ML_Syntax.print_list ML_Syntax.print_string)) (name, kind))
47.53 + | (name, NONE) => error ("Expected command keyword " ^ quote name)))));
47.54
47.55 end;
47.56
48.1 --- a/src/Pure/Proof/extraction.ML Fri Mar 16 16:32:34 2012 +0000
48.2 +++ b/src/Pure/Proof/extraction.ML Fri Mar 16 18:21:22 2012 +0100
48.3 @@ -820,25 +820,24 @@
48.4 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
48.5
48.6 val _ =
48.7 - Outer_Syntax.command "realizers"
48.8 - "specify realizers for primitive axioms / theorems, together with correctness proof"
48.9 - Keyword.thy_decl
48.10 + Outer_Syntax.command ("realizers", Keyword.thy_decl)
48.11 + "specify realizers for primitive axioms / theorems, together with correctness proof"
48.12 (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
48.13 (fn xs => Toplevel.theory (fn thy => add_realizers
48.14 (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
48.15
48.16 val _ =
48.17 - Outer_Syntax.command "realizability"
48.18 - "add equations characterizing realizability" Keyword.thy_decl
48.19 - (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
48.20 + Outer_Syntax.command ("realizability", Keyword.thy_decl)
48.21 + "add equations characterizing realizability"
48.22 + (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
48.23
48.24 val _ =
48.25 - Outer_Syntax.command "extract_type"
48.26 - "add equations characterizing type of extracted program" Keyword.thy_decl
48.27 - (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
48.28 + Outer_Syntax.command ("extract_type", Keyword.thy_decl)
48.29 + "add equations characterizing type of extracted program"
48.30 + (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
48.31
48.32 val _ =
48.33 - Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
48.34 + Outer_Syntax.command ("extract", Keyword.thy_decl) "extract terms from proofs"
48.35 (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
48.36 extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
48.37
49.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 16 16:32:34 2012 +0000
49.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 16 18:21:22 2012 +0100
49.3 @@ -189,31 +189,31 @@
49.4 (* additional outer syntax for Isar *)
49.5
49.6 val _ =
49.7 - Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
49.8 + Outer_Syntax.improper_command ("ProofGeneral.pr", Keyword.diag) "print state (internal)"
49.9 (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
49.10 if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
49.11 else (Toplevel.quiet := false; Toplevel.print_state true state))));
49.12
49.13 val _ = (*undo without output -- historical*)
49.14 - Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
49.15 + Outer_Syntax.improper_command ("ProofGeneral.undo", Keyword.control) "(internal)"
49.16 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
49.17
49.18 val _ =
49.19 - Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
49.20 + Outer_Syntax.improper_command ("ProofGeneral.restart", Keyword.control) "(internal)"
49.21 (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
49.22
49.23 val _ =
49.24 - Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
49.25 + Outer_Syntax.improper_command ("ProofGeneral.kill_proof", Keyword.control) "(internal)"
49.26 (Scan.succeed (Toplevel.no_timing o
49.27 Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
49.28
49.29 val _ =
49.30 - Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
49.31 + Outer_Syntax.improper_command ("ProofGeneral.inform_file_processed", Keyword.control) "(internal)"
49.32 (Parse.name >> (fn file =>
49.33 Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
49.34
49.35 val _ =
49.36 - Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
49.37 + Outer_Syntax.improper_command ("ProofGeneral.inform_file_retracted", Keyword.control) "(internal)"
49.38 (Parse.name >> (Toplevel.no_timing oo
49.39 (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
49.40
50.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 16 16:32:34 2012 +0000
50.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 16 18:21:22 2012 +0100
50.3 @@ -1032,7 +1032,7 @@
50.4 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
50.5
50.6 val _ =
50.7 - Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
50.8 + Outer_Syntax.improper_command ("ProofGeneral.process_pgip", Keyword.control) "(internal)"
50.9 (Parse.text >> (Toplevel.no_timing oo
50.10 (fn txt => Toplevel.imperative (fn () =>
50.11 if print_mode_active proof_general_emacsN
51.1 --- a/src/Pure/System/isar.ML Fri Mar 16 16:32:34 2012 +0000
51.2 +++ b/src/Pure/System/isar.ML Fri Mar 16 18:21:22 2012 +0100
51.3 @@ -164,35 +164,36 @@
51.4 (* global history *)
51.5
51.6 val _ =
51.7 - Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
51.8 + Outer_Syntax.improper_command ("init_toplevel", Keyword.control) "init toplevel point-of-interest"
51.9 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
51.10
51.11 val _ =
51.12 - Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
51.13 + Outer_Syntax.improper_command ("linear_undo", Keyword.control) "undo commands"
51.14 (Scan.optional Parse.nat 1 >>
51.15 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
51.16
51.17 val _ =
51.18 - Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
51.19 + Outer_Syntax.improper_command ("undo", Keyword.control) "undo commands (skipping closed proofs)"
51.20 (Scan.optional Parse.nat 1 >>
51.21 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
51.22
51.23 val _ =
51.24 - Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
51.25 - Keyword.control
51.26 + Outer_Syntax.improper_command ("undos_proof", Keyword.control)
51.27 + "undo commands (skipping closed proofs)"
51.28 (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
51.29 Toplevel.keep (fn state =>
51.30 if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
51.31
51.32 val _ =
51.33 - Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
51.34 - Keyword.control
51.35 + Outer_Syntax.improper_command ("cannot_undo", Keyword.control)
51.36 + "partial undo -- Proof General legacy"
51.37 (Parse.name >>
51.38 (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
51.39 | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
51.40
51.41 val _ =
51.42 - Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
51.43 + Outer_Syntax.improper_command ("kill", Keyword.control)
51.44 + "kill partial proof or theory development"
51.45 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
51.46
51.47 end;
52.1 --- a/src/Pure/System/session.ML Fri Mar 16 16:32:34 2012 +0000
52.2 +++ b/src/Pure/System/session.ML Fri Mar 16 18:21:22 2012 +0100
52.3 @@ -48,7 +48,7 @@
52.4 (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
52.5
52.6 val _ =
52.7 - Outer_Syntax.improper_command "welcome" "print welcome message" Keyword.diag
52.8 + Outer_Syntax.improper_command ("welcome", Keyword.diag) "print welcome message"
52.9 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
52.10
52.11
53.1 --- a/src/Pure/Thy/thy_header.ML Fri Mar 16 16:32:34 2012 +0000
53.2 +++ b/src/Pure/Thy/thy_header.ML Fri Mar 16 18:21:22 2012 +0100
53.3 @@ -8,13 +8,13 @@
53.4 sig
53.5 type header =
53.6 {name: string, imports: string list,
53.7 - keywords: (string * (string * string list) option) list,
53.8 + keywords: (string * Keyword.spec option) list,
53.9 uses: (Path.T * bool) list}
53.10 - val make: string -> string list -> (string * (string * string list) option) list ->
53.11 + val make: string -> string list -> (string * Keyword.spec option) list ->
53.12 (Path.T * bool) list -> header
53.13 val define_keywords: header -> unit
53.14 - val declare_keyword: string * (string * string list) option -> theory -> theory
53.15 - val the_keyword: theory -> string -> Keyword.T option
53.16 + val declare_keyword: string * Keyword.spec option -> theory -> theory
53.17 + val the_keyword: theory -> string -> Keyword.spec option
53.18 val args: header parser
53.19 val read: Position.T -> string -> header
53.20 end;
53.21 @@ -24,7 +24,7 @@
53.22
53.23 type header =
53.24 {name: string, imports: string list,
53.25 - keywords: (string * (string * string list) option) list,
53.26 + keywords: (string * Keyword.spec option) list,
53.27 uses: (Path.T * bool) list};
53.28
53.29 fun make name imports keywords uses : header =
53.30 @@ -35,26 +35,27 @@
53.31 (** keyword declarations **)
53.32
53.33 fun define_keywords ({keywords, ...}: header) =
53.34 - List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords;
53.35 + List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
53.36
53.37 fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
53.38
53.39 structure Data = Theory_Data
53.40 (
53.41 - type T = Keyword.T option Symtab.table;
53.42 + type T = Keyword.spec option Symtab.table;
53.43 val empty = Symtab.empty;
53.44 val extend = I;
53.45 fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
53.46 );
53.47
53.48 -fun declare_keyword (name, decl) = Data.map (fn data =>
53.49 - let val kind = Option.map Keyword.make decl
53.50 - in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
53.51 +fun declare_keyword (name, spec) =
53.52 + Data.map (fn data =>
53.53 + (Option.map Keyword.spec spec;
53.54 + Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
53.55
53.56 fun the_keyword thy name =
53.57 (case Symtab.lookup (Data.get thy) name of
53.58 - SOME kind => kind
53.59 - | NONE => error ("Unknown outer syntax keyword " ^ quote name));
53.60 + SOME spec => spec
53.61 + | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
53.62
53.63
53.64
54.1 --- a/src/Pure/Tools/find_consts.ML Fri Mar 16 16:32:34 2012 +0000
54.2 +++ b/src/Pure/Tools/find_consts.ML Fri Mar 16 18:21:22 2012 +0100
54.3 @@ -135,7 +135,7 @@
54.4 in
54.5
54.6 val _ =
54.7 - Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
54.8 + Outer_Syntax.improper_command ("find_consts", Keyword.diag) "search constants by type pattern"
54.9 (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
54.10 >> (fn spec => Toplevel.no_timing o
54.11 Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
55.1 --- a/src/Pure/Tools/find_theorems.ML Fri Mar 16 16:32:34 2012 +0000
55.2 +++ b/src/Pure/Tools/find_theorems.ML Fri Mar 16 18:21:22 2012 +0100
55.3 @@ -612,8 +612,8 @@
55.4 val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
55.5
55.6 val _ =
55.7 - Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
55.8 - Keyword.diag
55.9 + Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
55.10 + "print theorems meeting specified criteria"
55.11 (options -- query_parser
55.12 >> (fn ((opt_lim, rem_dups), spec) =>
55.13 Toplevel.no_timing o
56.1 --- a/src/Tools/Code/code_haskell.ML Fri Mar 16 16:32:34 2012 +0000
56.2 +++ b/src/Tools/Code/code_haskell.ML Fri Mar 16 18:21:22 2012 +0100
56.3 @@ -449,10 +449,9 @@
56.4 (** Isar setup **)
56.5
56.6 val _ =
56.7 - Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
56.8 - Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
56.9 - Toplevel.theory (add_monad target raw_bind))
56.10 - );
56.11 + Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
56.12 + (Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
56.13 + Toplevel.theory (add_monad target raw_bind)));
56.14
56.15 val setup =
56.16 Code_Target.add_target
57.1 --- a/src/Tools/Code/code_preproc.ML Fri Mar 16 16:32:34 2012 +0000
57.2 +++ b/src/Tools/Code/code_preproc.ML Fri Mar 16 18:21:22 2012 +0100
57.3 @@ -525,8 +525,8 @@
57.4 end;
57.5
57.6 val _ =
57.7 - Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
57.8 - Keyword.diag (Scan.succeed
57.9 + Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
57.10 + (Scan.succeed
57.11 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
57.12 (print_codeproc o Toplevel.theory_of)));
57.13
58.1 --- a/src/Tools/Code/code_runtime.ML Fri Mar 16 16:32:34 2012 +0000
58.2 +++ b/src/Tools/Code/code_runtime.ML Fri Mar 16 18:21:22 2012 +0100
58.3 @@ -352,13 +352,14 @@
58.4 in
58.5
58.6 val _ =
58.7 - Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
58.8 - Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
58.9 + Outer_Syntax.command @{command_spec "code_reflect"}
58.10 + "enrich runtime environment with generated code"
58.11 + (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
58.12 ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
58.13 -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
58.14 -- Scan.option (@{keyword "file"} |-- Parse.name)
58.15 - >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
58.16 - (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
58.17 + >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
58.18 + (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
58.19
58.20 end; (*local*)
58.21
59.1 --- a/src/Tools/Code/code_target.ML Fri Mar 16 16:32:34 2012 +0000
59.2 +++ b/src/Tools/Code/code_target.ML Fri Mar 16 18:21:22 2012 +0100
59.3 @@ -680,57 +680,54 @@
59.4 -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
59.5
59.6 val _ =
59.7 - Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
59.8 - process_multi_syntax Parse.xname (Scan.option Parse.string)
59.9 - add_class_syntax_cmd);
59.10 + Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
59.11 + (process_multi_syntax Parse.xname (Scan.option Parse.string)
59.12 + add_class_syntax_cmd);
59.13
59.14 val _ =
59.15 - Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
59.16 - process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
59.17 + Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
59.18 + (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
59.19 (Scan.option (Parse.minus >> K ()))
59.20 - add_instance_syntax_cmd);
59.21 + add_instance_syntax_cmd);
59.22
59.23 val _ =
59.24 - Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
59.25 - process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
59.26 - add_tyco_syntax_cmd);
59.27 + Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
59.28 + (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
59.29 + add_tyco_syntax_cmd);
59.30
59.31 val _ =
59.32 - Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
59.33 - process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
59.34 - add_const_syntax_cmd);
59.35 + Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
59.36 + (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
59.37 + add_const_syntax_cmd);
59.38
59.39 val _ =
59.40 - Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
59.41 - Keyword.thy_decl (
59.42 - Parse.name -- Scan.repeat1 Parse.name
59.43 - >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
59.44 - );
59.45 + Outer_Syntax.command @{command_spec "code_reserved"}
59.46 + "declare words as reserved for target language"
59.47 + (Parse.name -- Scan.repeat1 Parse.name
59.48 + >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
59.49
59.50 val _ =
59.51 - Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
59.52 - Keyword.thy_decl (
59.53 - Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
59.54 - | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
59.55 - >> (fn ((target, name), content_consts) =>
59.56 - (Toplevel.theory o add_include_cmd target) (name, content_consts))
59.57 - );
59.58 + Outer_Syntax.command @{command_spec "code_include"}
59.59 + "declare piece of code to be included in generated code"
59.60 + (Parse.name -- Parse.name -- (Parse.text :|--
59.61 + (fn "-" => Scan.succeed NONE
59.62 + | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
59.63 + >> (fn ((target, name), content_consts) =>
59.64 + (Toplevel.theory o add_include_cmd target) (name, content_consts)));
59.65
59.66 val _ =
59.67 - Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
59.68 - Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
59.69 - >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
59.70 - );
59.71 + Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
59.72 + (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
59.73 + >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames));
59.74
59.75 val _ =
59.76 - Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
59.77 - Keyword.thy_decl (
59.78 - Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
59.79 - );
59.80 + Outer_Syntax.command @{command_spec "code_abort"}
59.81 + "permit constant to be implemented as program abort"
59.82 + (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd));
59.83
59.84 val _ =
59.85 - Outer_Syntax.command "export_code" "generate executable code for constants"
59.86 - Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
59.87 + Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
59.88 + (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
59.89
59.90 end; (*local*)
59.91
60.1 --- a/src/Tools/Code/code_thingol.ML Fri Mar 16 16:32:34 2012 +0000
60.2 +++ b/src/Tools/Code/code_thingol.ML Fri Mar 16 18:21:22 2012 +0100
60.3 @@ -1046,14 +1046,15 @@
60.4 in
60.5
60.6 val _ =
60.7 - Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
60.8 + Outer_Syntax.improper_command @{command_spec "code_thms"}
60.9 + "print system of code equations for code"
60.10 (Scan.repeat1 Parse.term_group
60.11 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
60.12 o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
60.13
60.14 val _ =
60.15 - Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
60.16 - Keyword.diag
60.17 + Outer_Syntax.improper_command @{command_spec "code_deps"}
60.18 + "visualize dependencies of code equations for code"
60.19 (Scan.repeat1 Parse.term_group
60.20 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
60.21 o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
61.1 --- a/src/Tools/induct.ML Fri Mar 16 16:32:34 2012 +0000
61.2 +++ b/src/Tools/induct.ML Fri Mar 16 18:21:22 2012 +0100
61.3 @@ -259,8 +259,9 @@
61.4 end;
61.5
61.6 val _ =
61.7 - Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
61.8 - Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
61.9 + Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
61.10 + "print induction and cases rules"
61.11 + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
61.12 Toplevel.keep (print_rules o Toplevel.context_of)));
61.13
61.14
62.1 --- a/src/Tools/interpretation_with_defs.ML Fri Mar 16 16:32:34 2012 +0000
62.2 +++ b/src/Tools/interpretation_with_defs.ML Fri Mar 16 18:21:22 2012 +0100
62.3 @@ -80,8 +80,8 @@
62.4 end;
62.5
62.6 val _ =
62.7 - Outer_Syntax.command "interpretation"
62.8 - "prove interpretation of locale expression in theory" Keyword.thy_goal
62.9 + Outer_Syntax.command @{command_spec "interpretation"}
62.10 + "prove interpretation of locale expression in theory"
62.11 (Parse.!!! (Parse_Spec.locale_expression true) --
62.12 Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
62.13 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
63.1 --- a/src/Tools/quickcheck.ML Fri Mar 16 16:32:34 2012 +0000
63.2 +++ b/src/Tools/quickcheck.ML Fri Mar 16 18:21:22 2012 +0100
63.3 @@ -83,7 +83,6 @@
63.4 struct
63.5
63.6 val quickcheckN = "quickcheck"
63.7 -val quickcheck_paramsN = "quickcheck_params"
63.8
63.9 val genuineN = "genuine"
63.10 val noneN = "none"
63.11 @@ -530,11 +529,12 @@
63.12 @{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
63.13
63.14 val _ =
63.15 - Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
63.16 + Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
63.17 (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
63.18
63.19 val _ =
63.20 - Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
63.21 + Outer_Syntax.improper_command @{command_spec "quickcheck"}
63.22 + "try to find counterexample for subgoal"
63.23 (parse_args -- Scan.optional Parse.nat 1
63.24 >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
63.25
64.1 --- a/src/Tools/solve_direct.ML Fri Mar 16 16:32:34 2012 +0000
64.2 +++ b/src/Tools/solve_direct.ML Fri Mar 16 18:21:22 2012 +0100
64.3 @@ -107,10 +107,9 @@
64.4 val solve_direct = do_solve_direct Normal
64.5
64.6 val _ =
64.7 - Outer_Syntax.improper_command solve_directN
64.8 - "try to solve conjectures directly with existing theorems" Keyword.diag
64.9 - (Scan.succeed
64.10 - (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
64.11 + Outer_Syntax.improper_command @{command_spec "solve_direct"}
64.12 + "try to solve conjectures directly with existing theorems"
64.13 + (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
64.14
64.15
64.16 (* hook *)
65.1 --- a/src/Tools/subtyping.ML Fri Mar 16 16:32:34 2012 +0000
65.2 +++ b/src/Tools/subtyping.ML Fri Mar 16 18:21:22 2012 +0100
65.3 @@ -1028,10 +1028,10 @@
65.4 (* outer syntax commands *)
65.5
65.6 val _ =
65.7 - Outer_Syntax.improper_command "print_coercions" "print all coercions" Keyword.diag
65.8 + Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions"
65.9 (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)))
65.10 val _ =
65.11 - Outer_Syntax.improper_command "print_coercion_maps" "print all coercion maps" Keyword.diag
65.12 + Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps"
65.13 (Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of)))
65.14
65.15 end;
66.1 --- a/src/Tools/try.ML Fri Mar 16 16:32:34 2012 +0000
66.2 +++ b/src/Tools/try.ML Fri Mar 16 18:21:22 2012 +0100
66.3 @@ -88,9 +88,9 @@
66.4 |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
66.5
66.6 val _ =
66.7 - Outer_Syntax.improper_command tryN
66.8 - "try a combination of automatic proving and disproving tools" Keyword.diag
66.9 - (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
66.10 + Outer_Syntax.improper_command @{command_spec "try"}
66.11 + "try a combination of automatic proving and disproving tools"
66.12 + (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
66.13
66.14
66.15 (* automatic try *)
67.1 --- a/src/Tools/value.ML Fri Mar 16 16:32:34 2012 +0000
67.2 +++ b/src/Tools/value.ML Fri Mar 16 18:21:22 2012 +0100
67.3 @@ -63,7 +63,7 @@
67.4 Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
67.5
67.6 val _ =
67.7 - Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
67.8 + Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
67.9 (opt_evaluator -- opt_modes -- Parse.term
67.10 >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
67.11 (value_cmd some_name modes t)));
68.1 --- a/src/ZF/Tools/datatype_package.ML Fri Mar 16 16:32:34 2012 +0000
68.2 +++ b/src/ZF/Tools/datatype_package.ML Fri Mar 16 18:21:22 2012 +0100
68.3 @@ -430,19 +430,18 @@
68.4 Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
68.5 Parse.opt_mixfix >> Parse.triple1;
68.6
68.7 -val datatype_decl =
68.8 - (Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
68.9 - Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
68.10 - Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
68.11 - Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
68.12 - Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
68.13 - >> (Toplevel.theory o mk_datatype);
68.14 -
68.15 val coind_prefix = if coind then "co" else "";
68.16
68.17 val _ =
68.18 - Outer_Syntax.command (coind_prefix ^ "datatype")
68.19 - ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
68.20 + Outer_Syntax.command
68.21 + (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
68.22 + ("define " ^ coind_prefix ^ "datatype")
68.23 + ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
68.24 + Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
68.25 + Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
68.26 + Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
68.27 + Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
68.28 + >> (Toplevel.theory o mk_datatype));
68.29
68.30 end;
68.31
69.1 --- a/src/ZF/Tools/ind_cases.ML Fri Mar 16 16:32:34 2012 +0000
69.2 +++ b/src/ZF/Tools/ind_cases.ML Fri Mar 16 18:21:22 2012 +0100
69.3 @@ -65,8 +65,8 @@
69.4 (* outer syntax *)
69.5
69.6 val _ =
69.7 - Outer_Syntax.command "inductive_cases"
69.8 - "create simplified instances of elimination rules (improper)" Keyword.thy_script
69.9 + Outer_Syntax.command @{command_spec "inductive_cases"}
69.10 + "create simplified instances of elimination rules (improper)"
69.11 (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
69.12 >> (Toplevel.theory o inductive_cases));
69.13
70.1 --- a/src/ZF/Tools/induct_tacs.ML Fri Mar 16 16:32:34 2012 +0000
70.2 +++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 16 18:21:22 2012 +0100
70.3 @@ -188,16 +188,13 @@
70.4
70.5 (* outer syntax *)
70.6
70.7 -val rep_datatype_decl =
70.8 - (@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
70.9 - (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
70.10 - (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
70.11 - Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
70.12 - >> (fn (((x, y), z), w) => rep_datatype x y z w);
70.13 -
70.14 val _ =
70.15 - Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
70.16 - (rep_datatype_decl >> Toplevel.theory);
70.17 + Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
70.18 + ((@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
70.19 + (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
70.20 + (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
70.21 + Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
70.22 + >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
70.23
70.24 end;
70.25
71.1 --- a/src/ZF/Tools/inductive_package.ML Fri Mar 16 16:32:34 2012 +0000
71.2 +++ b/src/ZF/Tools/inductive_package.ML Fri Mar 16 18:21:22 2012 +0100
71.3 @@ -591,8 +591,9 @@
71.4 >> (Toplevel.theory o mk_ind);
71.5
71.6 val _ =
71.7 - Outer_Syntax.command (co_prefix ^ "inductive")
71.8 - ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
71.9 + Outer_Syntax.command
71.10 + (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
71.11 + ("define " ^ co_prefix ^ "inductive sets") ind_decl;
71.12
71.13 end;
71.14
72.1 --- a/src/ZF/Tools/primrec_package.ML Fri Mar 16 16:32:34 2012 +0000
72.2 +++ b/src/ZF/Tools/primrec_package.ML Fri Mar 16 18:21:22 2012 +0100
72.3 @@ -196,8 +196,7 @@
72.4 (* outer syntax *)
72.5
72.6 val _ =
72.7 - Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
72.8 - Keyword.thy_decl
72.9 + Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
72.10 (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
72.11 >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
72.12
73.1 --- a/src/ZF/Tools/typechk.ML Fri Mar 16 16:32:34 2012 +0000
73.2 +++ b/src/ZF/Tools/typechk.ML Fri Mar 16 18:21:22 2012 +0100
73.3 @@ -121,7 +121,7 @@
73.4 "ZF type-checking";
73.5
73.6 val _ =
73.7 - Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
73.8 + Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
73.9 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
73.10 Toplevel.keep (print_tcset o Toplevel.context_of)));
73.11