# HG changeset patch
# User wenzelm
# Date 1695563742 -7200
# Node ID e10ef4f9c84847ac381ee7fe6775257bbd27b69a
# Parent  37b49c592265d24f22f3aa7dc353f017961b0ef0
clarified signature;

diff -r 37b49c592265 -r e10ef4f9c848 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Sep 24 15:14:45 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Sep 24 15:55:42 2023 +0200
@@ -970,11 +970,7 @@
     fun err () = error "The provided bundle is not a lifting bundle"
   in
     (case bundle of
-      [(_, [arg_src])] => 
-        let
-          val (name, _) = Token.syntax (Scan.lift Parse.string) arg_src ctxt
-            handle ERROR _ => err ()
-        in name end
+      [(_, [arg_src])] => (Token.read ctxt Parse.string arg_src handle ERROR _ => err ())
     | _ => err ())
   end
 
diff -r 37b49c592265 -r e10ef4f9c848 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Sep 24 15:14:45 2023 +0200
+++ b/src/Pure/Isar/parse.ML	Sun Sep 24 15:55:42 2023 +0200
@@ -534,7 +534,7 @@
   end;
 
 fun read_embedded_src ctxt keywords parse src =
-  Token.syntax (Scan.lift embedded_input) src ctxt
-  |> #1 |> read_embedded ctxt keywords parse;
+  Token.read ctxt embedded_input src
+  |> read_embedded ctxt keywords parse;
 
 end;
diff -r 37b49c592265 -r e10ef4f9c848 src/Pure/Isar/token.ML
--- 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;
diff -r 37b49c592265 -r e10ef4f9c848 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:14:45 2023 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:55:42 2023 +0200
@@ -71,7 +71,7 @@
   ML_Context.add_antiquotation binding true
     (fn _ => fn src => fn ctxt =>
       let
-        val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt;
+        val s = Token.read ctxt Parse.embedded_input src;
         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 Parse.embedded_input) src ctxt in
+      let val s = Token.read ctxt Parse.embedded_input src in
         if check ctxt then ML_Context.read_antiquotes s ctxt
         else (K ([], []), ctxt)
       end);
diff -r 37b49c592265 -r e10ef4f9c848 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 15:14:45 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 15:55:42 2023 +0200
@@ -348,7 +348,7 @@
   ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
     (fn _ => fn src => fn ctxt =>
       let
-        val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt;
+        val s = Token.read ctxt Parse.embedded_input src;
         val tokenize = ML_Lex.tokenize_no_range;
 
         val (decl, ctxt') = ML_Context.read_antiquotes s ctxt;
diff -r 37b49c592265 -r e10ef4f9c848 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Sun Sep 24 15:14:45 2023 +0200
+++ b/src/Pure/Thy/term_style.ML	Sun Sep 24 15:55:42 2023 +0200
@@ -34,7 +34,7 @@
   Parse.token Parse.name ::: Parse.args >> (fn src0 =>
     let
       val (src, parse) = Token.check_src ctxt get_data src0;
-      val (f, _) = Token.syntax (Scan.lift parse) src ctxt;
+      val f = Token.read ctxt parse src;
     in f ctxt end);
 
 val parse = Args.context :|-- (fn ctxt => Scan.lift