# HG changeset patch
# User wenzelm
# Date 1187021422 -7200
# Node ID 4ffeb1dd048a38281c7525357879a8fe03dd72b3
# Parent  d7ee11ba1534d0ff151b65bd445cd8e3baf588e0
Lexicon.tokenize: do not appen EndToken yet;

diff -r d7ee11ba1534 -r 4ffeb1dd048a src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Aug 13 18:10:22 2007 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Aug 13 18:10:22 2007 +0200
@@ -275,7 +275,7 @@
       Scan.one Symbol.is_blank >> K NONE;
   in
     (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
-      (toks, []) => map_filter I toks @ [EndToken]
+      (toks, []) => map_filter I toks
     | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
   end;
 
diff -r d7ee11ba1534 -r 4ffeb1dd048a src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Aug 13 18:10:22 2007 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Aug 13 18:10:22 2007 +0200
@@ -882,7 +882,7 @@
 
 fun parse (Gram {tags, prods, chains, ...}) start toks =
 let val r =
-  (case earley prods tags chains start toks of
+  (case earley prods tags chains start (toks @ [Lexicon.EndToken]) of
     [] => sys_error "parse: no parse trees"
   | pts => pts);
 in r end