--- a/src/Pure/Isar/token.ML Sun Sep 24 15:14:45 2023 +0200
+++ b/src/Pure/Isar/token.ML Sun Sep 24 15:55:42 2023 +0200
@@ -111,6 +111,7 @@
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
+ val read: Proof.context -> 'a parser -> src -> 'a
end;
structure Token: TOKEN =
@@ -833,6 +834,8 @@
fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
+fun read ctxt scan src = syntax (Scan.lift scan) src ctxt |> #1;
+
end;
type 'a parser = 'a Token.parser;