# HG changeset patch
# User wenzelm
# Date 1218233376 -7200
# Node ID 0d0adaf0228d67270787a6d668a3c66c6088401b
# Parent  df444ddeff566b6a7476b50be8e9427d914782b2
datatype token: maintain range, tuned representation;
tuned messages;

diff -r df444ddeff56 -r 0d0adaf0228d src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Aug 09 00:09:35 2008 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Aug 09 00:09:36 2008 +0200
@@ -54,8 +54,8 @@
                          lambda productions are stored as normal productions
                          and also as an entry in "lambdas"*)
 
-val UnknownStart = EndToken;       (*productions for which no starting token is
-                                     known yet are associated with this token*)
+val UnknownStart = eof;       (*productions for which no starting token is
+                                known yet are associated with this token*)
 
 (* get all NTs that are connected with a list of NTs
    (used for expanding chain list)*)
@@ -395,7 +395,7 @@
 
     val nt_name = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
 
-    fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s)
+    fun pretty_symb (Terminal (Token (Literal, s, _))) = Pretty.quote (Pretty.str s)
       | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
       | pretty_symb (Nonterminal (tag, p)) = Pretty.str (nt_name tag ^ "[" ^ string_of_int p ^ "]");
 
@@ -455,7 +455,7 @@
       nonterminals are converted to integer tags*)
     fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
       | symb_of ((Delim s) :: ss) nt_count tags result =
-          symb_of ss nt_count tags ((Terminal (Token s)) :: result)
+          symb_of ss nt_count tags (Terminal (Token (Literal, s, Position.no_range)) :: result)
       | symb_of ((Argument (s, p)) :: ss) nt_count tags result =
           let
             val (nt_count', tags', new_symb) =
@@ -787,17 +787,14 @@
   (case Array.sub (stateset, i) of
     [] =>
       let
-        val toks =
-          if prev_token = EndToken then indata
-          else prev_token :: indata;
-
-        val msg =
-          if null toks then Pretty.str "Inner syntax error: unexpected end of input"
-          else
-            Pretty.block (Pretty.str "Inner syntax error at: \"" ::
-              Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))) @
-              [Pretty.str "\""]);
-      in error (Pretty.string_of msg) end
+        val toks = if is_eof prev_token then indata else prev_token :: indata;
+        val pos = pos_of_token prev_token;
+      in
+        if null toks then error ("Inner syntax error: unexpected end of input" ^ pos)
+        else error (Pretty.string_of (Pretty.block
+          (Pretty.str ("Inner syntax error" ^ pos ^ " at: ") ::
+            Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))))))
+      end
   | s =>
     (case indata of
        [] => Array.sub (stateset, i)
@@ -818,29 +815,33 @@
                        SOME tag => tag
                      | NONE   => error ("parse: Unknown startsymbol " ^
                                         quote startsymbol);
-    val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal EndToken],
-               "", 0)];
+    val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
   in
     Array.update (Estate, 0, S0);
-    get_trees (produce (ref false) prods tags chains Estate 0 indata EndToken)
+    get_trees (produce (ref false) prods tags chains Estate 0 indata eof)
   end;
 
 
 fun parse (Gram {tags, prods, chains, ...}) start toks =
-let val r =
-  (case earley prods tags chains start (toks @ [Lexicon.EndToken]) of
-    [] => sys_error "parse: no parse trees"
-  | pts => pts);
-in r end;
+  let
+    val end_pos =
+      (case try List.last toks of
+        NONE => Position.none
+      | SOME (Token (_, _, (_, end_pos))) => end_pos);
+    val r =
+      (case earley prods tags chains start (toks @ [mk_eof end_pos]) of
+        [] => sys_error "parse: no parse trees"
+      | pts => pts);
+  in r end;
 
 
 fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
   let
     fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1);
-    val prods = (maps snd o maps snd o freeze o #prods) gram;
-    fun guess (SOME ([Nonterminal (_, k), Terminal (Token s), Nonterminal (_, l)], _, j)) =
+    val prods = maps snd (maps snd (freeze (#prods gram)));
+    fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
           if k = j andalso l = j + 1 then SOME (s, true, false, j)
           else if k = j + 1 then if l = j then SOME (s, false, true, j)
             else if l = j + 1 then SOME (s, false, false, j)