# HG changeset patch
# User wenzelm
# Date 1698055718 -7200
# Node ID 30bcf149054d35308a686da9da4795329ef5c176
# Parent  f0cb320603cb8bae7a90fb936b603fc8e5bbc32a
clarified modules;

diff -r f0cb320603cb -r 30bcf149054d src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sun Oct 22 19:40:28 2023 +0200
+++ b/src/Pure/General/scan.ML	Mon Oct 23 12:08:38 2023 +0200
@@ -14,6 +14,7 @@
   type message = unit -> string
   (*error msg handler*)
   val !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b
+  val !!! : string -> ('a -> string option) -> ('a -> 'b) -> 'a -> 'b
   (*apply function*)
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   (*alternative*)
@@ -107,6 +108,20 @@
 exception ABORT of message;  (*dead end*)
 
 fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
+
+fun !!! prefix input_position scan =
+  let
+    fun print_position inp = the_default " (end-of-input)" (input_position inp);
+
+    fun err (inp, NONE) = (fn () => prefix ^ print_position inp)
+      | err (inp, SOME msg) =
+          (fn () =>
+            let val s = msg () in
+              if String.isPrefix prefix s then s
+              else prefix ^ print_position inp ^ ": " ^ s
+            end);
+  in !! err scan end;
+
 fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE;
 fun strict scan xs = scan xs handle MORE () => raise FAIL NONE;
 fun error scan xs = scan xs handle ABORT msg => Exn.error (msg ());
diff -r f0cb320603cb -r 30bcf149054d src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Oct 22 19:40:28 2023 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Oct 23 12:08:38 2023 +0200
@@ -147,22 +147,8 @@
 
 (* cut *)
 
-fun cut kind scan =
-  let
-    fun get_pos [] = " (end-of-input)"
-      | get_pos (tok :: _) = Position.here (Token.pos_of tok);
-
-    fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
-      | err (toks, SOME msg) =
-          (fn () =>
-            let val s = msg () in
-              if String.isPrefix kind s then s
-              else kind ^ get_pos toks ^ ": " ^ s
-            end);
-  in Scan.!! err scan end;
-
-fun !!! scan = cut "Outer syntax error" scan;
-fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
+fun !!! scan = Scan.!!! "Outer syntax error" Token.input_position scan;
+fun !!!! scan = Scan.!!! "Corrupted outer syntax in presentation" Token.input_position scan;
 
 
 
diff -r f0cb320603cb -r 30bcf149054d src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sun Oct 22 19:40:28 2023 +0200
+++ b/src/Pure/Isar/token.ML	Mon Oct 23 12:08:38 2023 +0200
@@ -35,6 +35,7 @@
     Output of XML.body option
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
+  val input_position: src -> string option
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -215,6 +216,9 @@
 fun adjust_offsets adjust (Token ((x, range), y, z)) =
   Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
 
+fun input_position [] = NONE
+  | input_position (tok :: _) = SOME (Position.here (pos_of tok));
+
 
 (* stopper *)
 
diff -r f0cb320603cb -r 30bcf149054d src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Oct 22 19:40:28 2023 +0200
+++ b/src/Pure/Tools/rail.ML	Mon Oct 23 12:08:38 2023 +0200
@@ -142,21 +142,10 @@
 
 (* parser combinators *)
 
-fun !!! scan =
-  let
-    val prefix = "Rail syntax error";
-
-    fun get_pos [] = " (end-of-input)"
-      | get_pos (tok :: _) = Position.here (pos_of tok);
+fun input_position [] = NONE
+  | input_position (tok :: _) = SOME (Position.here (pos_of tok));
 
-    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
-      | err (toks, SOME msg) =
-          (fn () =>
-            let val s = msg () in
-              if String.isPrefix prefix s then s
-              else prefix ^ get_pos toks ^ ": " ^ s
-            end);
-  in Scan.!! err scan end;
+fun !!! scan = Scan.!!! "Rail syntax error" input_position scan;
 
 fun $$$ x =
   Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||