# HG changeset patch
# User wenzelm
# Date 1698058376 -7200
# Node ID b8775a63cb35796a5c131df4a30112125767c7d6
# Parent  aff231884b20bbbd51356232749fe7086188cda0
proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);

diff -r aff231884b20 -r b8775a63cb35 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Oct 23 12:11:39 2023 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Oct 23 12:52:56 2023 +0200
@@ -8,6 +8,7 @@
 sig
   val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
+  val !!!! : (Context.generic * Token.src -> 'a) -> Context.generic * Token.src -> 'a
   val not_eof: Token.T parser
   val token: 'a parser -> Token.T parser
   val range: 'a parser -> ('a * Position.range) parser
@@ -146,7 +147,10 @@
 
 (* cut *)
 
-fun !!! scan = Scan.!!! "Outer syntax error" Token.input_position scan;
+val err_prefix = "Outer syntax error";
+
+fun !!! scan = Scan.!!! err_prefix Token.input_position scan;
+fun !!!! scan = Scan.!!! err_prefix Token.context_input_position scan;
 
 
 
@@ -236,7 +240,7 @@
 fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
-fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
+fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- !!!! scan);
 fun enum' sep scan = enum1' sep scan || Scan.succeed [];
 
 fun and_list1 scan = enum1 "and" scan;
diff -r aff231884b20 -r b8775a63cb35 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Oct 23 12:11:39 2023 +0200
+++ b/src/Pure/Isar/token.ML	Mon Oct 23 12:52:56 2023 +0200
@@ -36,6 +36,7 @@
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
   val input_position: src -> string option
+  val context_input_position: Context.generic * src -> string option
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -219,6 +220,9 @@
 fun input_position [] = NONE
   | input_position (tok :: _) = SOME (Position.here (pos_of tok));
 
+fun context_input_position (_: Context.generic, []) = NONE
+  | context_input_position (_, tok :: _) = SOME (Position.here (pos_of tok));
+
 
 (* stopper *)