clarified modules;
authorwenzelm
Wed, 20 Oct 2021 20:25:33 +0200
changeset 74563 042041c0ebeb
parent 74562 8403bd51f8b1
child 74564 0a66a61e740c
clarified modules;
src/CCL/CCL.thy
src/CCL/Wfd.thy
src/CTT/CTT.thy
src/Doc/Prog_Prove/LaTeXsugar.thy
src/FOL/FOL.thy
src/HOL/Eisbach/parse_tools.ML
src/HOL/HOLCF/IOA/CompoScheds.thy
src/HOL/HOLCF/IOA/Sequence.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/UNITY/UNITY_Main.thy
src/LCF/LCF.thy
src/Pure/Isar/args.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/parse.ML
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/ML/ml_thms.ML
src/Pure/PIDE/resources.ML
src/Pure/System/scala_compiler.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Tools/jedit.ML
src/Pure/Tools/named_theorems.ML
src/Pure/Tools/plugin.ML
src/Pure/Tools/rule_insts.ML
src/Pure/simplifier.ML
src/Tools/induct_tacs.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/UNITY/SubstAx.thy
--- 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"