--- 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 ());
--- 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;
--- 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 *)
--- 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) ||