# HG changeset patch
# User wenzelm
# Date 1634740609 -7200
# Node ID 44dc1661a5cb442d87691d590c72efe8d0a56bb0
# Parent  59febd85a0f61d0b37fc3932453c4f459b0e9ac2
clarified signature;

diff -r 59febd85a0f6 -r 44dc1661a5cb src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Oct 20 11:34:28 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Oct 20 16:36:49 2021 +0200
@@ -35,13 +35,15 @@
 
 (* concrete syntax *)
 
-val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>);
-
 fun read_actions str =
   let
-    val actions = Token.read_body keywords
+    val thy = \<^theory>;
+    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
       (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params))
-      (Symbol_Pos.explode0 str)
+      (Input.string str)
     fun split_name_label (name, args) labels =
         (case String.tokens (fn c => c = #".") name of
           [name] => (("", name, args), labels)
@@ -53,7 +55,8 @@
            ((label, name, args), Symtab.insert_set label labels))
         | _ => error "Cannot parse action")
   in
-    Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty)) actions
+    try read_actions ()
+    |> Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty))
   end
 
 
diff -r 59febd85a0f6 -r 44dc1661a5cb src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Oct 20 11:34:28 2021 +0200
+++ b/src/Pure/Isar/method.ML	Wed Oct 20 16:36:49 2021 +0200
@@ -735,12 +735,9 @@
     val src2 = map Token.closure src1;
   in (text, src2) end;
 
-fun read_closure_input ctxt input =
-  let val syms = Input.source_explode input in
-    (case Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.many Token.not_eof) syms of
-      SOME res => read_closure ctxt res
-    | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
-  end;
+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;
 
 val text_closure =
   Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
diff -r 59febd85a0f6 -r 44dc1661a5cb src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Oct 20 11:34:28 2021 +0200
+++ b/src/Pure/Isar/token.ML	Wed Oct 20 16:36:49 2021 +0200
@@ -104,8 +104,8 @@
   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_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option
   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,17 +766,32 @@
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
 
-(* read body -- e.g. antiquotation source *)
-
-fun read_body keywords scan =
-  tokenize (Keyword.no_command_keywords keywords) {strict = true}
-  #> filter is_proper
-  #> Scan.read stopper scan;
+(* embedded source, e.g. for antiquotations *)
 
 fun read_antiq keywords scan (syms, pos) =
-  (case read_body keywords scan syms of
-    SOME x => x
-  | NONE => error ("Malformed antiquotation" ^ Position.here 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 *)
diff -r 59febd85a0f6 -r 44dc1661a5cb src/Pure/Thy/document_marker.ML
--- a/src/Pure/Thy/document_marker.ML	Wed Oct 20 11:34:28 2021 +0200
+++ b/src/Pure/Thy/document_marker.ML	Wed Oct 20 16:36:49 2021 +0200
@@ -59,11 +59,11 @@
 
     val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker));
 
+    val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords' ctxt);
     val body = Symbol_Pos.cartouche_content syms;
     val markers =
-      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
-        SOME res => res
-      | NONE => error ("Bad input" ^ Position.here pos));
+      Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body)
+      |> Token.read_embedded ctxt keywords (Parse.list parse_marker);
   in
     ctxt
     |> Config.put config_command_name cmd_name