# HG changeset patch
# User wenzelm
# Date 1634832651 -7200
# Node ID 0a66a61e740cbef0721c1e18b49b59ecc959a2f4
# Parent  042041c0ebeb1fef9fe8fc1d5c7af3c0ff9a7360
clarified modules;

diff -r 042041c0ebeb -r 0a66a61e740c src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -41,7 +41,7 @@
     val ctxt = Proof_Context.init_global thy
     val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords thy)
 
-    fun read_actions () = Token.read_embedded ctxt keywords
+    fun read_actions () = Parse.read_embedded ctxt keywords
       (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params))
       (Input.string str)
     fun split_name_label (name, args) labels =
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Isar/method.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -741,7 +741,7 @@
 
 fun read_closure_input ctxt =
   let val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords' ctxt)
-  in Token.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end;
+  in Parse.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end;
 
 val text_closure =
   Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -121,6 +121,9 @@
   val options: ((string * Position.T) * (string * Position.T)) list parser
   val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
   val embedded_ml_underscore: ML_Lex.token Antiquote.antiquote list parser
+  val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
+  val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
+  val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a
 end;
 
 structure Parse: PARSE =
@@ -508,4 +511,35 @@
 val embedded_ml_underscore =
   input underscore >> ML_Lex.read_source || embedded_ml;
 
+
+(* read embedded source, e.g. for antiquotations *)
+
+fun read_antiq keywords scan (syms, pos) =
+  let
+    val toks = syms
+      |> Token.tokenize (Keyword.no_command_keywords keywords) {strict = true}
+      |> filter Token.is_proper;
+  in
+    (case Scan.read Token.stopper scan toks of
+      SOME res => res
+    | NONE => error ("Malformed antiquotation" ^ Position.here pos))
+  end;
+
+fun read_embedded ctxt keywords parse input =
+  let
+    val toks = input
+      |> Input.source_explode
+      |> Token.tokenize keywords {strict = true}
+      |> filter Token.is_proper;
+    val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
+  in
+    (case Scan.read Token.stopper parse toks of
+      SOME res => res
+    | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
+  end;
+
+fun read_embedded_src ctxt keywords parse src =
+  Token.syntax (Scan.lift embedded_input) src ctxt
+  |> #1 |> read_embedded ctxt keywords parse;
+
 end;
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Isar/token.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -104,8 +104,6 @@
   val make_src: string * Position.T -> T list -> src
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
-  val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
-  val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
@@ -766,33 +764,6 @@
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
 
-(* embedded source, e.g. for antiquotations *)
-
-fun read_antiq keywords scan (syms, pos) =
-  let
-    val toks = syms
-      |> tokenize (Keyword.no_command_keywords keywords) {strict = true}
-      |> filter is_proper;
-  in
-    (case Scan.read stopper scan toks of
-      SOME res => res
-    | NONE => error ("Malformed antiquotation" ^ Position.here pos))
-  end;
-
-fun read_embedded ctxt keywords parse input =
-  let
-    val toks = input
-      |> Input.source_explode
-      |> tokenize keywords {strict = true}
-      |> filter is_proper;
-    val _ = Context_Position.reports_text ctxt (maps (reports keywords) toks);
-  in
-    (case Scan.read stopper parse toks of
-      SOME res => res
-    | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
-  end;
-
-
 (* wrapped syntax *)
 
 fun syntax_generic scan src context =
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -221,10 +221,6 @@
 
 (* type/term constructors *)
 
-fun read_embedded ctxt keywords parse src =
-  Token.syntax (Scan.lift Parse.embedded_input) src ctxt
-  |> #1 |> Token.read_embedded ctxt keywords parse;
-
 local
 
 val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;
@@ -257,7 +253,7 @@
     (fn range => fn src => fn ctxt =>
       let
         val ((s, type_args), fn_body) = src
-          |> read_embedded ctxt keywords (parse_name -- parse_args -- parse_body function);
+          |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function);
         val pos = Input.pos_of s;
 
         val Type (c, Ts) =
@@ -292,7 +288,7 @@
     (fn range => fn src => fn ctxt =>
       let
         val (((s, type_args), term_args), fn_body) = src
-          |> read_embedded ctxt keywords
+          |> Parse.read_embedded_src ctxt keywords
               (parse_name -- parse_args -- parse_for_args -- parse_body function);
 
         val Const (c, T) =
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -111,7 +111,7 @@
         (Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   | Antiquote.Antiq {range, body, ...} =>
       ctxt |> apply_antiquotation range
-        (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)));
+        (Parse.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)));
 
 in
 
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -188,7 +188,7 @@
 in
 
 fun read_antiq ctxt ({range = (pos, _), body, ...}: Antiquote.antiq) =
-  Token.read_antiq (Thy_Header.get_keywords' ctxt) parse_antiq (body, pos);
+  Parse.read_antiq (Thy_Header.get_keywords' ctxt) parse_antiq (body, pos);
 
 fun evaluate eval_text ctxt antiq =
   (case antiq of
diff -r 042041c0ebeb -r 0a66a61e740c src/Pure/Thy/document_marker.ML
--- a/src/Pure/Thy/document_marker.ML	Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Thy/document_marker.ML	Thu Oct 21 18:10:51 2021 +0200
@@ -62,7 +62,7 @@
     val body = Symbol_Pos.cartouche_content syms;
     val markers =
       Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body)
-      |> Token.read_embedded ctxt keywords (Parse.list parse_marker);
+      |> Parse.read_embedded ctxt keywords (Parse.list parse_marker);
   in
     ctxt
     |> Config.put config_command_name cmd_name