theory Scratch
   imports
     Main
begin

ML‹
fun get_tokens_pos [] = " (end-of-input)"
   | get_tokens_pos (tok :: _) = Position.here (Token.pos_of tok);

(*generalisation of Parse.cut*)
fun cut get_pos kind scan =
   let
     fun err (x, NONE) = (fn () => kind ^ get_pos x)
       | err (x, SOME msg) =
           (fn () =>
             let val s = msg () in
               if String.isPrefix kind s then s
               else kind ^ get_pos x ^ ": " ^ s
             end);
   in Scan.!! err scan end;

local
val error_msg = "Outer syntax error";
in
fun !!! scan = cut get_tokens_pos error_msg scan;
(*!!! for context parsers (currently missing in the standard distribution)*)
fun !!!+ scan = cut (get_tokens_pos o snd) error_msg scan;
end

(*same definition as Parse.enum1*)
fun enum1 sep scan = scan ::: Scan.repeat (Parse.$$$ sep |-- !!! scan);
(*now including cuts (unlike Parse.enum1')*)
fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift (Parse.$$$ sep)
|-- !!!+ scan);
(*current definition of Parse.enum1'*)
(* fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |--
scan); *)

(*example attributes to show parsing differences*)
val _ =
   Theory.setup (
     Attrib.setup \<^binding>‹withcut›
       (enum1' "and" (Scan.lift Parse.nat) |-- Scan.succeed (K (NONE,
NONE)))
       "withcut"
     #> Attrib.setup \<^binding>‹withoutcut›
       (Parse.enum1' "and" (Scan.lift Parse.nat) |-- Scan.succeed (K
(NONE, NONE)))
       "withoutcut"
   )
›

(*
error/squiggly line at "this is not a nat"; error message:
Outer syntax error⌂: natural number expected,
but quoted string "this is not a nat"⌂ was found
*)
declare [[withcut 0 and "this is not a nat"]]
(*
error/squiggly line at "withoutcut"; error message:
Bad arguments for attribute "withoutcut"⌂:
   and "this is not a nat"
*)
declare [[withoutcut 0 and "this is not a nat"]]

end