--- a/src/CCL/CCL.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/CCL/CCL.thy Wed Oct 20 20:25:33 2021 +0200
@@ -474,7 +474,7 @@
done
method_setup eq_coinduct3 = \<open>
- Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
+ Scan.lift Parse.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD'
(Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
\<close>
--- a/src/CCL/Wfd.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/CCL/Wfd.thy Wed Oct 20 20:25:33 2021 +0200
@@ -47,7 +47,7 @@
done
method_setup wfd_strengthen = \<open>
- Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
+ Scan.lift Parse.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
THEN assume_tac ctxt (i + 1)))
--- a/src/CTT/CTT.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/CTT/CTT.thy Wed Oct 20 20:25:33 2021 +0200
@@ -450,7 +450,7 @@
method_setup eqintr = \<open>Scan.succeed (SIMPLE_METHOD o eqintr_tac)\<close>
method_setup NE = \<open>
- Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
+ Scan.lift Parse.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
\<close>
method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Wed Oct 20 20:25:33 2021 +0200
@@ -45,7 +45,7 @@
setup \<open>
Document_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close>
- (Scan.lift Args.embedded_inner_syntax)
+ (Scan.lift Parse.embedded_inner_syntax)
(fn ctxt => fn c =>
let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",
--- a/src/FOL/FOL.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/FOL/FOL.thy Wed Oct 20 20:25:33 2021 +0200
@@ -72,7 +72,7 @@
\<close>
method_setup case_tac = \<open>
- Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
+ Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
\<close> "case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Eisbach/parse_tools.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML Wed Oct 20 20:25:33 2021 +0200
@@ -36,7 +36,7 @@
(fn ((_, SOME t), _) => Real_Val t
| ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Term t)) tok)));
-val name_term = parse_term_val Args.embedded_inner_syntax;
+val name_term = parse_term_val Parse.embedded_inner_syntax;
fun parse_thm_val scan =
Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option (Args.internal_fact >> the_single)) -- scan >>
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy Wed Oct 20 20:25:33 2021 +0200
@@ -289,7 +289,7 @@
\<close>
method_setup mkex_induct = \<open>
- Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
+ Scan.lift (Parse.embedded -- Parse.embedded -- Parse.embedded)
>> (fn ((sch, exA), exB) => fn ctxt =>
SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
\<close>
--- a/src/HOL/HOLCF/IOA/Sequence.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Wed Oct 20 20:25:33 2021 +0200
@@ -996,13 +996,13 @@
\<close>
method_setup Seq_case =
- \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
+ \<open>Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
method_setup Seq_case_simp =
- \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
+ \<open>Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
method_setup Seq_induct =
- \<open>Scan.lift Args.embedded --
+ \<open>Scan.lift Parse.embedded --
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close>
@@ -1010,10 +1010,10 @@
\<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close>
method_setup pair =
- \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
+ \<open>Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
method_setup pair_induct =
- \<open>Scan.lift Args.embedded --
+ \<open>Scan.lift Parse.embedded --
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
--- a/src/HOL/Library/LaTeXsugar.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Wed Oct 20 20:25:33 2021 +0200
@@ -98,7 +98,7 @@
setup \<open>
Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
- (Scan.lift Args.embedded_inner_syntax)
+ (Scan.lift Parse.embedded_inner_syntax)
(fn ctxt => fn c =>
let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",
--- a/src/HOL/UNITY/UNITY_Main.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Wed Oct 20 20:25:33 2021 +0200
@@ -16,7 +16,7 @@
"for proving safety properties"
method_setup ensures_tac = \<open>
- Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
+ Args.goal_spec -- Scan.lift Parse.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
\<close> "for proving progress properties"
--- a/src/LCF/LCF.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/LCF/LCF.thy Wed Oct 20 20:25:33 2021 +0200
@@ -319,7 +319,7 @@
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
method_setup induct = \<open>
- Scan.lift Args.embedded_inner_syntax >> (fn v => fn ctxt =>
+ Scan.lift Parse.embedded_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN
REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
--- a/src/Pure/Isar/args.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Isar/args.ML Wed Oct 20 20:25:33 2021 +0200
@@ -28,11 +28,6 @@
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
val text_token: Token.T parser
- val embedded_token: Token.T parser
- val embedded_inner_syntax: string parser
- val embedded_input: Input.source parser
- val embedded: string parser
- val embedded_position: (string * Position.T) parser
val text_input: Input.source parser
val text: string parser
val binding: binding parser
@@ -115,13 +110,7 @@
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_input = cartouche >> Token.input_of;
-val embedded_token = ident || string || cartouche;
-val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of;
-val embedded_input = embedded_token >> Token.input_of;
-val embedded = embedded_token >> Token.content_of;
-val embedded_position = embedded_input >> Input.source_content;
-
-val text_token = embedded_token || Parse.token Parse.verbatim;
+val text_token = Parse.token (Parse.embedded || Parse.verbatim);
val text_input = text_token >> Token.input_of;
val text = text_token >> Token.content_of;
@@ -151,10 +140,12 @@
internal_source || name_token >> Token.evaluate Token.Source read;
fun named_typ read =
- internal_typ || embedded_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
+ internal_typ ||
+ Parse.token Parse.embedded >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
fun named_term read =
- internal_term || embedded_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
+ internal_term ||
+ Parse.token Parse.embedded >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
fun named_fact get =
internal_fact ||
--- a/src/Pure/Isar/locale.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Isar/locale.ML Wed Oct 20 20:25:33 2021 +0200
@@ -187,7 +187,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
- (Args.theory -- Scan.lift Args.embedded_position >>
+ (Args.theory -- Scan.lift Parse.embedded_position >>
(ML_Syntax.print_string o uncurry check)));
fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy);
--- a/src/Pure/Isar/method.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Isar/method.ML Wed Oct 20 20:25:33 2021 +0200
@@ -427,7 +427,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
- (Args.context -- Scan.lift Args.embedded_position >>
+ (Args.context -- Scan.lift Parse.embedded_position >>
(ML_Syntax.print_string o uncurry check_name)));
--- a/src/Pure/Isar/parse.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Isar/parse.ML Wed Oct 20 20:25:33 2021 +0200
@@ -67,6 +67,7 @@
val name_position: (string * Position.T) parser
val binding: binding parser
val embedded: string parser
+ val embedded_inner_syntax: string parser
val embedded_input: Input.source parser
val embedded_position: (string * Position.T) parser
val text: string parser
@@ -281,6 +282,7 @@
(cartouche || string || short_ident || long_ident || sym_ident ||
term_var || type_ident || type_var || number);
+val embedded_inner_syntax = inner_syntax embedded;
val embedded_input = input embedded;
val embedded_position = embedded_input >> Input.source_content;
--- a/src/Pure/ML/ml_antiquotation.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Wed Oct 20 20:25:33 2021 +0200
@@ -71,7 +71,7 @@
ML_Context.add_antiquotation binding true
(fn _ => fn src => fn ctxt =>
let
- val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt;
+ val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt;
val tokenize = ML_Lex.tokenize_no_range;
val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
@@ -89,7 +89,7 @@
fun conditional binding check =
ML_Context.add_antiquotation binding true
(fn _ => fn src => fn ctxt =>
- let val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt in
+ let val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt in
if check ctxt then
ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt
else (K ([], []), ctxt)
@@ -106,7 +106,7 @@
inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
value_embedded (Binding.make ("binding", \<^here>))
- (Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #>
+ (Scan.lift Parse.embedded_input >> (ML_Syntax.make_binding o Input.source_content)) #>
value_embedded (Binding.make ("cartouche", \<^here>))
(Scan.lift Args.cartouche_input >> (fn source =>
@@ -114,6 +114,6 @@
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
inline_embedded (Binding.make ("verbatim", \<^here>))
- (Scan.lift Args.embedded >> ML_Syntax.print_string));
+ (Scan.lift Parse.embedded >> ML_Syntax.print_string));
end;
--- a/src/Pure/ML/ml_antiquotations.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Wed Oct 20 20:25:33 2021 +0200
@@ -23,7 +23,7 @@
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
ML_Antiquotation.declaration_embedded \<^binding>\<open>print\<close>
- (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
+ (Scan.lift (Scan.optional Parse.embedded "Output.writeln"))
(fn src => fn output => fn ctxt =>
let
val struct_name = ML_Context.struct_name ctxt;
@@ -52,18 +52,18 @@
val _ = Theory.setup
(ML_Antiquotation.value_embedded \<^binding>\<open>system_option\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
ML_Antiquotation.value_embedded \<^binding>\<open>theory\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
"Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
@@ -90,14 +90,14 @@
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>oracle_name\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos)))));
(* schematic variables *)
val schematic_input =
- Args.context -- Scan.lift Args.embedded_input >> (fn (ctxt, src) =>
+ Args.context -- Scan.lift Parse.embedded_input >> (fn (ctxt, src) =>
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt,
(Syntax.implode_input src, Input.pos_of src)));
@@ -116,7 +116,7 @@
(* type classes *)
-fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
+fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) =>
Proof_Context.read_class ctxt s
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
@@ -126,13 +126,13 @@
ML_Antiquotation.inline_embedded \<^binding>\<open>class_syntax\<close> (class true) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>sort\<close>
- (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
+ (Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) =>
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
(* type constructors *)
-fun type_name kind check = Args.context -- Scan.lift Args.embedded_token
+fun type_name kind check = Args.context -- Scan.lift (Parse.token Parse.embedded)
>> (fn (ctxt, tok) =>
let
val s = Token.inner_syntax_of tok;
@@ -158,7 +158,7 @@
(* constants *)
-fun const_name check = Args.context -- Scan.lift Args.embedded_token
+fun const_name check = Args.context -- Scan.lift (Parse.token Parse.embedded)
>> (fn (ctxt, tok) =>
let
val s = Token.inner_syntax_of tok;
@@ -177,11 +177,11 @@
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #>
ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
+ (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax) -- Scan.optional
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, (raw_c, pos)), Ts) =>
let
@@ -222,7 +222,7 @@
(* type/term constructors *)
fun read_embedded ctxt keywords parse src =
- Token.syntax (Scan.lift Args.embedded_input) src ctxt
+ Token.syntax (Scan.lift Parse.embedded_input) src ctxt
|> #1 |> Token.read_embedded ctxt keywords parse;
local
--- a/src/Pure/ML/ml_thms.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/ML/ml_thms.ML Wed Oct 20 20:25:33 2021 +0200
@@ -77,7 +77,7 @@
val and_ = Args.$$$ "and";
val by = Parse.reserved "by";
-val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
+val goal = Scan.unless (by || and_) Parse.embedded_inner_syntax;
val _ = Theory.setup
(ML_Antiquotation.declaration \<^binding>\<open>lemma\<close>
--- a/src/Pure/PIDE/resources.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/PIDE/resources.ML Wed Oct 20 20:25:33 2021 +0200
@@ -203,7 +203,7 @@
(Args.context -- Scan.lift Parse.embedded_position
>> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #>
ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
let
val (name, multi) = check_scala_function ctxt arg;
val func = if multi then "Scala.function" else "Scala.function1";
--- a/src/Pure/System/scala_compiler.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/System/scala_compiler.ML Wed Oct 20 20:25:33 2021 +0200
@@ -66,21 +66,21 @@
val _ =
Theory.setup
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala\<close>
- (Scan.lift Args.embedded_position)
+ (Scan.lift Parse.embedded_position)
(fn _ => fn (s, pos) => (static_check (s, pos); s)) #>
Document_Output.antiquotation_raw_embedded \<^binding>\<open>scala_type\<close>
- (Scan.lift (Args.embedded_position -- (types >> print_types)))
+ (Scan.lift (Parse.embedded_position -- (types >> print_types)))
(fn _ => fn ((t, pos), type_args) =>
(static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args, pos);
scala_name (t ^ type_args))) #>
Document_Output.antiquotation_raw_embedded \<^binding>\<open>scala_object\<close>
- (Scan.lift Args.embedded_position)
+ (Scan.lift Parse.embedded_position)
(fn _ => fn (x, pos) => (static_check ("val _test_ = " ^ x, pos); scala_name x)) #>
Document_Output.antiquotation_raw_embedded \<^binding>\<open>scala_method\<close>
- (Scan.lift (class -- Args.embedded_position -- types -- args))
+ (Scan.lift (class -- Parse.embedded_position -- types -- args))
(fn _ => fn (((class_context, (method, pos)), method_types), method_args) =>
let
val class_types = (case class_context of SOME (_, Ts) => Ts | NONE => []);
--- a/src/Pure/Thy/document_antiquotations.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Wed Oct 20 20:25:33 2021 +0200
@@ -78,13 +78,13 @@
basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
- basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
+ basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Parse.embedded_inner_syntax) pretty_abbrev #>
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #>
- basic_entity \<^binding>\<open>bundle\<close> (Scan.lift Args.embedded_position) pretty_bundle #>
- basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
- basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #>
- basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #>
+ basic_entity \<^binding>\<open>locale\<close> (Scan.lift Parse.embedded_position) pretty_locale #>
+ basic_entity \<^binding>\<open>bundle\<close> (Scan.lift Parse.embedded_position) pretty_bundle #>
+ basic_entity \<^binding>\<open>class\<close> (Scan.lift Parse.embedded_inner_syntax) pretty_class #>
+ basic_entity \<^binding>\<open>type\<close> (Scan.lift Parse.embedded_inner_syntax) pretty_type #>
+ basic_entity \<^binding>\<open>theory\<close> (Scan.lift Parse.embedded_position) pretty_theory #>
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)
@@ -151,7 +151,7 @@
local
val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")");
-val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option index_like);
+val index_args = Parse.enum1 "!" (Parse.embedded_input -- Scan.option index_like);
fun output_text ctxt = Document_Output.output_document ctxt {markdown = false};
@@ -292,14 +292,14 @@
val _ = Theory.setup
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>bash_function\<close>
- (Scan.lift Args.embedded_position) Isabelle_System.check_bash_function);
+ (Scan.lift Parse.embedded_position) Isabelle_System.check_bash_function);
(* system options *)
val _ = Theory.setup
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>system_option\<close>
- (Scan.lift Args.embedded_position)
+ (Scan.lift Parse.embedded_position)
(fn ctxt => fn (name, pos) =>
let val _ = Completion.check_option (Options.default ()) ctxt (name, pos);
in name end));
@@ -418,7 +418,7 @@
translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c);
val _ = Theory.setup
- (Document_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_input)
+ (Document_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Parse.embedded_input)
(fn ctxt => fn source =>
let
val url = Input.string_of source;
--- a/src/Pure/Tools/jedit.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Tools/jedit.ML Wed Oct 20 20:25:33 2021 +0200
@@ -78,7 +78,8 @@
val _ =
Theory.setup
- (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
+ (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close>
+ (Scan.lift Parse.embedded_position)
(fn ctxt => fn (name, pos) =>
let
val _ =
--- a/src/Pure/Tools/named_theorems.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Tools/named_theorems.ML Wed Oct 20 20:25:33 2021 +0200
@@ -103,7 +103,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>named_theorems\<close>
- (Args.context -- Scan.lift Args.embedded_position >>
+ (Args.context -- Scan.lift Parse.embedded_position >>
(fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
end;
--- a/src/Pure/Tools/plugin.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Tools/plugin.ML Wed Oct 20 20:25:33 2021 +0200
@@ -40,7 +40,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>plugin\<close>
- (Args.context -- Scan.lift Args.embedded_position >> (ML_Syntax.print_string o uncurry check)));
+ (Args.context -- Scan.lift Parse.embedded_position >> (ML_Syntax.print_string o uncurry check)));
(* indirections *)
--- a/src/Pure/Tools/rule_insts.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML Wed Oct 20 20:25:33 2021 +0200
@@ -188,7 +188,7 @@
val named_insts =
Parse.and_list1
- (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax))
+ (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Parse.embedded_inner_syntax))
-- Parse.for_fixes;
val _ = Theory.setup
@@ -202,7 +202,7 @@
local
-val inst = Args.maybe Args.embedded_inner_syntax;
+val inst = Args.maybe Parse.embedded_inner_syntax;
val concl = Args.$$$ "concl" -- Args.colon;
val insts =
@@ -343,12 +343,12 @@
Method.setup \<^binding>\<open>cut_tac\<close> (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
Method.setup \<^binding>\<open>subgoal_tac\<close>
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Parse.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (props, fixes)) => fn ctxt =>
SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup \<^binding>\<open>thin_tac\<close>
- (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
"remove premise (dynamic instantiation)");
--- a/src/Pure/simplifier.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Pure/simplifier.ML Wed Oct 20 20:25:33 2021 +0200
@@ -114,7 +114,7 @@
val _ = Theory.setup
(ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
- (Args.context -- Scan.lift Args.embedded_position
+ (Args.context -- Scan.lift Parse.embedded_position
>> (fn (ctxt, name) =>
"Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
--- a/src/Tools/induct_tacs.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Tools/induct_tacs.ML Wed Oct 20 20:25:33 2021 +0200
@@ -122,14 +122,14 @@
val varss =
Parse.and_list'
- (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
+ (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Parse.embedded_inner_syntax))));
in
val _ =
Theory.setup
(Method.setup \<^binding>\<open>case_tac\<close>
- (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+ (Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
(fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
"unstructured case analysis on types" #>
Method.setup \<^binding>\<open>induct_tac\<close>
--- a/src/ZF/Tools/ind_cases.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/ZF/Tools/ind_cases.ML Wed Oct 20 20:25:33 2021 +0200
@@ -63,7 +63,7 @@
val _ =
Theory.setup
(Method.setup \<^binding>\<open>ind_cases\<close>
- (Scan.lift (Scan.repeat1 Args.embedded_inner_syntax) >>
+ (Scan.lift (Scan.repeat1 Parse.embedded_inner_syntax) >>
(fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
"dynamic case analysis on sets");
--- a/src/ZF/Tools/induct_tacs.ML Wed Oct 20 20:04:28 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Oct 20 20:25:33 2021 +0200
@@ -177,11 +177,11 @@
val _ =
Theory.setup
(Method.setup \<^binding>\<open>induct_tac\<close>
- (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Parse.embedded -- Parse.for_fixes) >>
(fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
"induct_tac emulation (dynamic instantiation!)" #>
Method.setup \<^binding>\<open>case_tac\<close>
- (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Parse.embedded -- Parse.for_fixes) >>
(fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
"datatype case_tac emulation (dynamic instantiation!)");
--- a/src/ZF/UNITY/SubstAx.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Wed Oct 20 20:25:33 2021 +0200
@@ -373,7 +373,7 @@
\<close>
method_setup ensures = \<open>
- Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
+ Args.goal_spec -- Scan.lift Parse.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
\<close> "for proving progress properties"