Add file name, line number and beginning of line position to locations.

Coq locations already had support for this, but were containing dummy
information. We now don't need anymore to reconstruct this information by
browsing the file when printing an error message or enriching exceptions on the
fly.

It also became easier to interface with Coq since locations emitted by the
lexer now always contain full information.

On the API side, Loc.represent disappeared and Loc.t is now exposed as record.
It is less error-prone than manipulating a tuple of 5 integers. Also,
Loc.create takes 5 arguments instead of 3 and a pair.

1 files changed, 177 insertions, 134 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 9a7aeaf0c..b04c7633a 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -9,6 +9,7 @@
 open Pp
 open Util
 open Tok
+open Compat
 
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
@@ -110,7 +111,12 @@ module Error = struct
 end
 open Error
 
-let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str)
+let current_file = ref ""
+
+let set_current_file ~fname =
+  current_file := fname
+
+let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
@@ -121,64 +127,68 @@ type token_kind =
   | AsciiChar
   | EmptyStream
 
-let error_unsupported_unicode_character n unicode cs =
+let error_unsupported_unicode_character loc n unicode cs =
   let bp = Stream.count cs in
-  err (bp,bp+n) (UnsupportedUnicode unicode)
+  let loc = set_loc_pos loc bp (bp+n) in
+  err loc (UnsupportedUnicode unicode)
 
-let error_utf8 cs =
+let error_utf8 loc cs =
   let bp = Stream.count cs in
   Stream.junk cs; (* consume the char to avoid read it and fail again *)
-  err (bp, bp+1) Illegal_character
+  let loc = set_loc_pos loc bp (bp+1) in
+  err loc Illegal_character
 
-let utf8_char_size cs = function
+let utf8_char_size loc cs = function
   (* Utf8 leading byte *)
   | '\x00'..'\x7F' -> 1
   | '\xC0'..'\xDF' -> 2
   | '\xE0'..'\xEF' -> 3
   | '\xF0'..'\xF7' -> 4
-  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs
+  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 loc cs
 
 let njunk n = Util.repeat n Stream.junk
 
-let check_utf8_trailing_byte cs c =
-  if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 cs
+let check_utf8_trailing_byte loc cs c =
+  if not (Int.equal (Char.code c land 0xC0) 0x80) then error_utf8 loc cs
 
 (* Recognize utf8 blocks (of length less than 4 bytes) *)
 (* but don't certify full utf8 compliance (e.g. no emptyness check) *)
-let lookup_utf8_tail c cs =
+let lookup_utf8_tail loc c cs =
   let c1 = Char.code c in
-  if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 cs
+  if Int.equal (c1 land 0x40) 0 || Int.equal (c1 land 0x38) 0x38 then error_utf8 loc cs
   else
     let n, unicode =
       if Int.equal (c1 land 0x20) 0 then
       match Stream.npeek 2 cs with
       | [_;c2] ->
-          check_utf8_trailing_byte cs c2;
+          check_utf8_trailing_byte loc cs c2;
           2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F)
-      | _ -> error_utf8 cs
+      | _ -> error_utf8 loc cs
       else if Int.equal (c1 land 0x10) 0 then
       match Stream.npeek 3 cs with
       | [_;c2;c3] ->
-          check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
+          check_utf8_trailing_byte loc cs c2;
+	  check_utf8_trailing_byte loc cs c3;
           3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 +
           (Char.code c3 land 0x3F)
-      | _ -> error_utf8 cs
+      | _ -> error_utf8 loc cs
       else match Stream.npeek 4 cs with
       | [_;c2;c3;c4] ->
-          check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
-          check_utf8_trailing_byte cs c4;
+          check_utf8_trailing_byte loc cs c2;
+	  check_utf8_trailing_byte loc cs c3;
+          check_utf8_trailing_byte loc cs c4;
           4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 +
           (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F)
-      | _ -> error_utf8 cs
+      | _ -> error_utf8 loc cs
     in
     try Unicode.classify unicode, n
     with Unicode.Unsupported ->
-      njunk n cs; error_unsupported_unicode_character n unicode cs
+      njunk n cs; error_unsupported_unicode_character loc n unicode cs
 
-let lookup_utf8 cs =
+let lookup_utf8 loc cs =
   match Stream.peek cs with
     | Some ('\x00'..'\x7F') -> AsciiChar
-    | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs)
+    | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail loc c cs)
     | None -> EmptyStream
 
 let unlocated f x = f x
@@ -189,7 +199,7 @@ let check_keyword str =
   let rec loop_symb = parser
     | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str
     | [< s >] ->
-        match unlocated lookup_utf8 s with
+        match unlocated lookup_utf8 Compat.CompatLoc.ghost s with
         | Utf8Token (_,n) -> njunk n s; loop_symb s
         | AsciiChar -> Stream.junk s; loop_symb s
         | EmptyStream -> ()
@@ -210,7 +220,7 @@ let check_ident str =
     | [< ' ('0'..'9' | ''') when intail; s >] ->
         loop_id true s
     | [< s >] ->
-        match unlocated lookup_utf8 s with
+        match unlocated lookup_utf8 Compat.CompatLoc.ghost s with
         | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s
         | Utf8Token (Unicode.IdentPart, n) when intail ->
           njunk n s;
@@ -263,13 +273,13 @@ let get_buff len = String.sub !buff 0 len
 
 (* The classical lexer: idents, numbers, quoted strings, comments *)
 
-let rec ident_tail len = parser
+let rec ident_tail loc len = parser
   | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] ->
-      ident_tail (store len c) s
+      ident_tail loc (store len c) s
   | [< s >] ->
-      match lookup_utf8 s with
+      match lookup_utf8 loc s with
       | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) ->
-          ident_tail (nstore n len s) s
+          ident_tail loc (nstore n len s) s
       | _ -> len
 
 let check_no_char s =
@@ -287,40 +297,43 @@ let is_gt3 = function
   | c::_ when c == '1' || c == '2' || c == '3' -> false
   | _ -> true
 
-let check_gt3 l loc len =
+let check_gt3 loc l len =
   if not (l == ['0']) && (is_teen l || is_gt3 l) then (false, len)
   else err loc (IncorrectIndex l)
 
-let check_n n l loc len =
+let check_n loc n l len =
   if List.hd l == n && not (is_teen l) then (false, len)
   else err loc (IncorrectIndex l)
 
-let rec number_or_index bp l len = parser
-  | [< ' ('0'..'9' as c); s >] -> number_or_index bp (c::l) (store len c) s
+let rec number_or_index loc bp l len = parser
+  | [< ' ('0'..'9' as c); s >] -> number_or_index loc bp (c::l) (store len c) s
   | [< s >] ep ->
+     let loc = set_loc_pos loc bp ep in
       match Stream.npeek 2 s with
-      | ['s';'t'] when check_no_char s -> njunk 2 s; check_n '1' l (bp,ep) len
-      | ['n';'d'] when check_no_char s -> njunk 2 s; check_n '2' l (bp,ep) len
-      | ['r';'d'] when check_no_char s -> njunk 2 s; check_n '3' l (bp,ep) len
-      | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 l (bp,ep) len
+      | ['s';'t'] when check_no_char s -> njunk 2 s; check_n loc '1' l len
+      | ['n';'d'] when check_no_char s -> njunk 2 s; check_n loc '2' l len
+      | ['r';'d'] when check_no_char s -> njunk 2 s; check_n loc '3' l len
+      | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len
       | _ -> true, len
 
-let rec string in_comments bp len = parser
+(* If the string being lexed is in a comment, [comm_level] is Some i with i the
+   current level of comments nesting. Otherwise, [comm_level] is None. *)
+let rec string loc ~comm_level bp len = parser
   | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
-      if esc then string in_comments bp (store len '"') s else len
+      if esc then string loc ~comm_level bp (store len '"') s else (loc, len)
   | [< ''('; s >] ->
       (parser
         | [< ''*'; s >] ->
-            string
-              (Option.map succ in_comments)
+            string loc
+              (Option.map succ comm_level)
               bp (store (store len '(') '*')
               s
         | [< >] ->
-            string in_comments bp (store len '(') s) s
+            string loc comm_level bp (store len '(') s) s
   | [< ''*'; s >] ->
       (parser
         | [< '')'; s >] ->
-            let () = match in_comments with
+            let () = match comm_level with
             | Some 0 ->
                 Feedback.msg_warning
                   (strbrk
@@ -329,12 +342,23 @@ let rec string in_comments bp len = parser
                       non-terminated string of the comment.")
             | _ -> ()
             in
-            let in_comments = Option.map pred in_comments in
-            string in_comments bp (store (store len '*') ')') s
+            let comm_level = Option.map pred comm_level in
+            string loc comm_level bp (store (store len '*') ')') s
         | [< >] ->
-            string in_comments bp (store len '*') s) s
-  | [< 'c; s >] -> string in_comments bp (store len c) s
-  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
+            string loc comm_level bp (store len '*') s) s
+  | [< ''\n' as c; s >] ep ->
+     (* If we are parsing a comment, the string if not part of a token so we
+     update the first line of the location. Otherwise, we update the last
+     line. *)
+     let loc =
+       if Option.has_some comm_level then bump_loc_line loc ep
+       else bump_loc_line_last loc ep
+     in
+     string loc comm_level bp (store len c) s
+  | [< 'c; s >] -> string loc comm_level bp (store len c) s
+  | [< _ = Stream.empty >] ep ->
+     let loc = set_loc_pos loc bp ep in
+     err loc Unterminated_string
 
 (* Hook for exporting comment into xml theory files *)
 let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
@@ -400,98 +424,109 @@ let comment_stop ep =
   between_com := false
 
 (* Does not unescape!!! *)
-let rec comm_string bp = parser
-  | [< ''"' >] -> push_string "\""
-  | [< ''\\'; _ =
+let rec comm_string loc bp = parser
+  | [< ''"' >] ep -> push_string "\""; loc
+  | [< ''\\'; loc =
            (parser [< ' ('"' | '\\' as c) >] ->
               let () = match c with
               | '"' -> real_push_char c
               | _ -> ()
               in
-              real_push_char c
-                 | [< >] -> real_push_char '\\'); s >]
-     -> comm_string bp s
-  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
-  | [< 'c; s >] -> real_push_char c; comm_string bp s
-
-let rec comment bp = parser bp2
+              real_push_char c; loc
+                 | [< >] -> real_push_char '\\'; loc); s >]
+     -> comm_string loc bp s
+  | [< _ = Stream.empty >] ep ->
+      let loc = set_loc_pos loc bp ep in
+      err loc Unterminated_string
+  | [< ''\n' as c; s >] ep -> real_push_char c; comm_string (bump_loc_line loc ep) bp s
+  | [< 'c; s >] -> real_push_char c; comm_string loc bp s
+
+let rec comment loc bp = parser bp2
   | [< ''(';
-       _ = (parser
-              | [< ''*'; s >] -> push_string "(*"; comment bp s
-              | [< >] -> push_string "(" );
-       s >] -> comment bp s
+       loc = (parser
+              | [< ''*'; s >] -> push_string "(*"; comment loc bp s
+              | [< >] -> push_string "("; loc );
+       s >] -> comment loc bp s
   | [< ''*';
-       _ = parser
-         | [< '')' >] -> push_string "*)";
-         | [< s >] -> real_push_char '*'; comment bp s >] -> ()
+       loc = parser
+         | [< '')' >] -> push_string "*)"; loc
+         | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc
   | [< ''"'; s >] ->
-      if Flags.do_beautify() then (push_string"\"";comm_string bp2 s)
-      else ignore (string (Some 0) bp2 0 s);
-      comment bp s
-  | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
-  | [< 'z; s >] -> real_push_char z; comment bp s
+      let loc =
+	(* In beautify mode, the lexing differs between strings in comments and
+	   regular strings (e.g. escaping). It seems wrong. *)
+	if Flags.do_beautify() then (push_string"\""; comm_string loc bp2 s)
+	else fst (string loc ~comm_level:(Some 0) bp2 0 s)
+      in
+      comment loc bp s
+  | [< _ = Stream.empty >] ep ->
+      let loc = set_loc_pos loc bp ep in
+      err loc Unterminated_comment
+  | [< ''\n' as z; s >] ep -> real_push_char z; comment (bump_loc_line loc ep) bp s
+  | [< 'z; s >] -> real_push_char z; comment loc bp s
 
 (* Parse a special token, using the [token_tree] *)
 
 (* Peek as much utf-8 lexemes as possible *)
 (* and retain the longest valid special token obtained *)
-let rec progress_further last nj tt cs =
-  try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
+let rec progress_further loc last nj tt cs =
+  try progress_from_byte loc last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
   with Failure _ -> last
 
-and update_longest_valid_token last nj tt cs =
+and update_longest_valid_token loc last nj tt cs =
   match tt.node with
   | Some _ as last' ->
     stream_njunk nj cs;
-    progress_further last' 0 tt cs
+    progress_further loc last' 0 tt cs
   | None ->
-    progress_further last nj tt cs
+    progress_further loc last nj tt cs
 
 (* nj is the number of char peeked since last valid token *)
 (* n the number of char in utf8 block *)
-and progress_utf8 last nj n c tt cs =
+and progress_utf8 loc last nj n c tt cs =
   try
     let tt = CharMap.find c tt.branch in
     if Int.equal n 1 then
-      update_longest_valid_token last (nj+n) tt cs
+      update_longest_valid_token loc last (nj+n) tt cs
     else
       match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with
       | l when Int.equal (List.length l) (n - 1) ->
-         List.iter (check_utf8_trailing_byte cs) l;
+         List.iter (check_utf8_trailing_byte loc cs) l;
          let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
-         update_longest_valid_token last (nj+n) tt cs
+         update_longest_valid_token loc last (nj+n) tt cs
       | _ ->
-          error_utf8 cs
+          error_utf8 loc cs
   with Not_found ->
     last
 
-and progress_from_byte last nj tt cs c =
-  progress_utf8 last nj (utf8_char_size cs c) c tt cs
+and progress_from_byte loc last nj tt cs c =
+  progress_utf8 loc last nj (utf8_char_size loc cs c) c tt cs
 
-let find_keyword id s =
+let find_keyword loc id s =
   let tt = ttree_find !token_tree id in
-  match progress_further tt.node 0 tt s with
+  match progress_further loc tt.node 0 tt s with
   | None -> raise Not_found
   | Some c -> KEYWORD c
 
-let process_sequence bp c cs =
+let process_sequence loc bp c cs =
   let rec aux n cs =
     match Stream.peek cs with
     | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs
-    | _ -> BULLET (String.make n c), (bp, Stream.count cs)
+    | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs)
   in
   aux 1 cs
 
 (* Must be a special token *)
-let process_chars bp c cs =
-  let t = progress_from_byte None (-1) !token_tree cs c in
+let process_chars loc bp c cs =
+  let t = progress_from_byte loc None (-1) !token_tree cs c in
   let ep = Stream.count cs in
   match t with
-    | Some t -> (KEYWORD t, (bp, ep))
+    | Some t -> (KEYWORD t, set_loc_pos loc bp ep)
     | None ->
-        let ep' = bp + utf8_char_size cs c in
+        let ep' = bp + utf8_char_size loc cs c in
         njunk (ep' - ep) cs;
-        err (bp, ep') Undefined_token
+	let loc = set_loc_pos loc bp ep' in
+        err loc Undefined_token
 
 let token_of_special c s = match c with
   | '.' -> FIELD s
@@ -499,27 +534,27 @@ let token_of_special c s = match c with
 
 (* Parse what follows a dot / a dollar *)
 
-let parse_after_special c bp =
+let parse_after_special loc c bp =
   parser
-  | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail (store 0 d) >] ->
+  | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d) >] ->
       token_of_special c (get_buff len)
   | [< s >] ->
-      match lookup_utf8 s with
+      match lookup_utf8 loc s with
       | Utf8Token (Unicode.Letter, n) ->
-          token_of_special c (get_buff (ident_tail (nstore n 0 s) s))
-      | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s)
+          token_of_special c (get_buff (ident_tail loc (nstore n 0 s) s))
+      | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s)
 
 (* Parse what follows a question mark *)
 
-let parse_after_qmark bp s =
+let parse_after_qmark loc bp s =
   match Stream.peek s with
     | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK
     | None -> KEYWORD "?"
     | _ ->
-        match lookup_utf8 s with
+        match lookup_utf8 loc s with
           | Utf8Token (Unicode.Letter, _) -> LEFTQMARK
           | AsciiChar | Utf8Token _ | EmptyStream ->
-            fst (process_chars bp '?' s)
+            fst (process_chars loc bp '?' s)
 
 let blank_or_eof cs =
   match Stream.peek cs with
@@ -529,69 +564,72 @@ let blank_or_eof cs =
 
 (* Parse a token in a char stream *)
 
-let rec next_token = parser bp
-  | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
-      comm_loc bp; push_char c; next_token s
-  | [< ''.' as c; t = parse_after_special c bp; s >] ep ->
+let rec next_token loc = parser bp
+  | [< ''\n' as c; s >] ep ->
+      comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s
+  | [< '' ' | '\t' | '\r' as c; s >] ->
+      comm_loc bp; push_char c; next_token loc s
+  | [< ''.' as c; t = parse_after_special loc c bp; s >] ep ->
       comment_stop bp;
       (* We enforce that "." should either be part of a larger keyword,
          for instance ".(", or followed by a blank or eof. *)
       let () = match t with
       | KEYWORD ("." | "...") ->
-        if not (blank_or_eof s) then err (bp,ep+1) Undefined_token;
-        between_com := true;
+        if not (blank_or_eof s) then
+	  err (set_loc_pos loc bp (ep+1)) Undefined_token;
+	between_com := true;
       | _ -> ()
       in
-      (t, (bp,ep))
+      (t, set_loc_pos loc bp ep)
   | [< ' ('-'|'+'|'*' as c); s >] ->
       let t,new_between_com =
-        if !between_com then process_sequence bp c s,true
-        else process_chars bp c s,false
+        if !between_com then process_sequence loc bp c s, true
+        else process_chars loc bp c s,false
       in
       comment_stop bp; between_com := new_between_com; t
   | [< ''?'; s >] ep ->
-      let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
+      let t = parse_after_qmark loc bp s in
+      comment_stop bp; (t, set_loc_pos loc ep bp)
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
-       len = ident_tail (store 0 c); s >] ep ->
+       len = ident_tail loc (store 0 c); s >] ep ->
       let id = get_buff len in
       comment_stop bp;
-      (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
-  | [< ' ('0'..'9' as c); (b,len) = number_or_index bp [c] (store 0 c) >] ep ->
+      (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
+  | [< ' ('0'..'9' as c); (b,len) = number_or_index loc bp [c] (store 0 c) >] ep ->
       comment_stop bp;
-      (if b then INT (get_buff len) else INDEX (get_buff len)), (bp, ep)
-  | [< ''\"'; len = string None bp 0 >] ep ->
+      (if b then INT (get_buff len) else INDEX (get_buff len)), set_loc_pos loc bp ep
+  | [< ''\"'; (loc,len) = string loc None bp 0 >] ep ->
       comment_stop bp;
-      (STRING (get_buff len), (bp, ep))
+      (STRING (get_buff len), set_loc_pos loc bp ep)
   | [< ' ('(' as c);
       t = parser
         | [< ''*'; s >] ->
             comm_loc bp;
             push_string "(*";
-            comment bp s;
-            next_token s
-        | [< t = process_chars bp c >] -> comment_stop bp; t >] ->
+            let loc = comment loc bp s in next_token loc s
+        | [< t = process_chars loc bp c >] -> comment_stop bp; t >] ->
       t
   | [< s >] ->
-      match lookup_utf8 s with
+      match lookup_utf8 loc s with
         | Utf8Token (Unicode.Letter, n) ->
-            let len = ident_tail (nstore n 0 s) s in
+            let len = ident_tail loc (nstore n 0 s) s in
             let id = get_buff len in
             let ep = Stream.count s in
             comment_stop bp;
-            (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
+            (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
         | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
-            let t = process_chars bp (Stream.next s) s in
+            let t = process_chars loc bp (Stream.next s) s in
             let new_between_com = match t with
               (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
             comment_stop bp; between_com := new_between_com; t
         | EmptyStream ->
-            comment_stop bp; (EOI, (bp, bp + 1))
+            comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
 
 (* (* Debug: uncomment this for tracing tokens seen by coq...*)
-let next_token s =
-  let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t);
-  (t,(bp,ep))
-*)
+let next_token loc s =
+  let (t,loc as r) = next_token loc s in
+  Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t);
+  r *)
 
 (* Location table system for creating tables associating a token count
    to its location in a char stream (the source) *)
@@ -640,11 +678,13 @@ let token_text = function
 
 let func cs =
   let loct = loct_create () in
+  let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
   let ts =
     Stream.from
       (fun i ->
-         let (tok, loc) = next_token cs in
-         loct_add loct i (Compat.make_loc loc); Some tok)
+         let (tok, loc) = next_token !cur_loc cs in
+	 cur_loc := Compat.after loc;
+         loct_add loct i loc; Some tok)
   in
   current_location_table := loct;
   (ts, loct_func loct)
@@ -680,16 +720,19 @@ module Token = struct
   end
 end
 
-let mk () _init_loc(*FIXME*) cs =
+let mk () =
   let loct = loct_create () in
-  let rec self =
+  let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
+  current_location_table := loct; 
+  let rec self init_loc (* FIXME *) =
     parser i
-       [< (tok, loc) = next_token; s >] ->
-          let loc = Compat.make_loc loc in
-            loct_add loct i loc;
-            [< '(tok, loc); self s >]
+       [< (tok, loc) = next_token !cur_loc; s >] ->
+            cur_loc := Compat.set_loc_file loc !current_file;
+	    loct_add loct i loc;
+            [< '(tok, loc); self init_loc s >]
       | [< >] -> [< >]
-  in current_location_table := loct; self cs
+  in
+  self
 
 END