# HG changeset patch
# User wenzelm
# Date 1727343103 -7200
# Node ID f9230aabcc2a109b811bcfff696a224ceab814f1
# Parent  6b8e746aed55f5b2276f5d9e1f5f927bb2b5767e
clarified use of Lexicon.dummy;
tuned signature;

diff -r 6b8e746aed55 -r f9230aabcc2a src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Sep 26 11:01:41 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Sep 26 11:31:43 2024 +0200
@@ -30,6 +30,7 @@
   val end_pos_of_token: token -> Position.T
   val is_proper: token -> bool
   val dummy: token
+  val is_dummy: token -> bool
   val literal: string -> token
   val is_literal: token -> bool
   val tokens_match_ord: token ord
@@ -144,7 +145,9 @@
 
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
-val dummy = Token (token_kind_index Dummy, "", Position.no_range);
+val dummy_index = token_kind_index Dummy;
+val dummy = Token (dummy_index, "", Position.no_range);
+fun is_dummy tok = index_of_token tok = dummy_index;
 
 
 (* literals *)
diff -r 6b8e746aed55 -r f9230aabcc2a src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Sep 26 11:01:41 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu Sep 26 11:31:43 2024 +0200
@@ -620,14 +620,14 @@
     Array.upd stateset (i + 1) Sii
   end;
 
-fun produce gram stateset i input prev_token =
+fun produce gram stateset i prev rest =
   (case Array.nth stateset i of
     [] =>
       let
-        val toks = if Lexicon.is_eof prev_token then input else prev_token :: input;
-        val pos = Position.here (Lexicon.pos_of_token prev_token);
+        val inp = if Lexicon.is_dummy prev then rest else prev :: rest;
+        val pos = Position.here (Lexicon.pos_of_token prev);
       in
-        if null toks then
+        if null inp then
           error ("Inner syntax error: unexpected end of input" ^ pos)
         else
           error ("Inner syntax error" ^ pos ^
@@ -637,13 +637,13 @@
                   Pretty.str "at", Pretty.brk 1,
                   Pretty.block
                    (Pretty.str "\"" ::
-                    Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
+                    Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last inp))) @
                     [Pretty.str "\""])])))
       end
   | states =>
-      (case input of
+      (case rest of
         [] => states
-      | c :: cs => (process_states gram stateset i c states; produce gram stateset (i + 1) cs c)));
+      | c :: cs => (process_states gram stateset i c states; produce gram stateset (i + 1) c cs)));
 
 in
 
@@ -665,7 +665,7 @@
     val _ = Array.upd stateset 0 [S0];
 
     val pts =
-      produce gram stateset 0 input Lexicon.eof
+      produce gram stateset 0 Lexicon.dummy input
       |> map_filter (fn (_, _, [pt]) => SOME pt | _ => NONE);
   in if null pts then raise Fail "Inner syntax: no parse trees" else pts end;