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.

3 files changed, 22 insertions, 67 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 1fe30217d..00e0219f1 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -152,38 +152,21 @@ let print_highlight_location ib loc =
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file {outer=s;inner=fname} loc =
-  let errstrm = str"Error while reading " ++ str s in
+let print_location_in_file loc =
+  let fname = loc.Loc.fname in
+  let errstrm = str"Error while reading " ++ str fname in
   if Loc.is_ghost loc then
     hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
   else
-    let errstrm =
-      if String.equal s fname then mt() else errstrm ++ str":" ++ fnl()
+    let errstrm = mt ()
+      (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *)
     in
-    let (bp,ep) = Loc.unloc loc in
-    let line_of_pos lin bol cnt =
-      try
-        let ic = open_in fname in
-        let rec line_of_pos lin bol cnt =
-          if cnt < bp then
-            if input_char ic == '\n'
-            then line_of_pos (lin + 1) (cnt +1) (cnt+1)
-            else line_of_pos lin bol (cnt+1)
-          else (lin, bol)
-        in
-        let rc = line_of_pos lin bol cnt in
-        close_in ic;
-        rc
-      with Sys_error _ -> 0, 0 in
-    try
-      let (line, bol) = line_of_pos 1 0 0 in
-      hov 0 (* No line break so as to follow emacs error message format *)
-        (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++
-           str", line " ++ int line ++ str", characters " ++
-           Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++
-        fnl ()
-    with e when Errors.noncritical e ->
-       hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()
+    let open Loc in
+    hov 0 (* No line break so as to follow emacs error message format *)
+	(errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+	   str", line " ++ int loc.line_nb ++ str", characters " ++
+	   Cerrors.print_loc (Loc.make_loc (loc.bp-loc.bol_pos,loc.ep-loc.bol_pos))) ++ str":" ++
+      fnl ()
 
 let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
@@ -264,12 +247,13 @@ let locate_exn = function
 
 let print_toplevel_error (e, info) =
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
-  let locmsg = match Vernac.get_exn_files info with
-    | Some files -> print_location_in_file files loc
-    | None ->
+  let fname = loc.Loc.fname in
+  let locmsg =
+    if String.equal fname "" then
       if locate_exn e && valid_buffer_loc top_buffer loc then
-        print_highlight_location top_buffer loc
+	print_highlight_location top_buffer loc
       else mt ()
+    else print_location_in_file loc
   in
   locmsg ++ Errors.iprint (e, info)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 94972e272..c8ea0f811 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -65,26 +65,6 @@ let _ =
       Goptions.optread  = (fun () -> !atomic_load);
       Goptions.optwrite = ((:=) atomic_load) }
 
-(* In case of error, register the file being currently Load'ed and the
-   inner file in which the error has been encountered. Any intermediate files
-   between the two are discarded. *)
-
-type location_files = { outer : string; inner : string }
-
-let files_of_exn : location_files Exninfo.t = Exninfo.make ()
-
-let get_exn_files e = Exninfo.get e files_of_exn
-
-let add_exn_files e f = Exninfo.add e files_of_exn f
-
-let enrich_with_file f (e, info) =
-  let inner = match get_exn_files info with None -> f | Some x -> x.inner in
-  (e, add_exn_files info { outer = f; inner })
-
-let raise_with_file f e = iraise (enrich_with_file f e)
-
-let cur_file = ref None
-
 let disable_drop = function
   | Drop -> Errors.error "Drop is forbidden."
   | e -> e
@@ -100,6 +80,7 @@ let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
+  CLexer.set_current_file longfname;
   let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
   (in_chan, longfname, (po, verb_ch))
 
@@ -244,7 +225,6 @@ and read_vernac_file verbosely s =
 	user_error loc "Navigation commands forbidden in files"
   in
   let (in_chan, fname, input) = open_file_twice_if verbosely s in
-  cur_file := Some fname;
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
@@ -258,10 +238,10 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
-          cur_file := None;
           if do_beautify () then
             pr_new_syntax (Loc.make_loc (max_int,max_int)) None
-      | _ -> raise_with_file fname (disable_drop e, info)
+      | reraise ->
+	 iraise (disable_drop e, info)
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
@@ -290,7 +270,7 @@ let load_vernac verb file =
   with any ->
     let (e, info) = Errors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
-    raise_with_file file (disable_drop e, info)
+    iraise (disable_drop e, info)
 
 let ensure_ext ext f =
   if Filename.check_suffix f ext then f
@@ -386,8 +366,5 @@ let compile v f =
   compile v f;
   CoqworkmgrApi.giveback 1
 
-let () = Hook.set Stm.process_error_hook (fun e ->
-  match !cur_file with
-  | None -> Cerrors.process_vernac_interp_error e
-  | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e)
-)
+let () = Hook.set Stm.process_error_hook
+  Cerrors.process_vernac_interp_error
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 008d7a31a..7bfddd947 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -38,9 +38,3 @@ val load_vernac : bool -> string -> unit
 val compile : bool -> string -> unit
 
 val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
-
-(** Has an exception been annotated with some file locations ? *)
-
-type location_files = { outer : string; inner : string }
-
-val get_exn_files : Exninfo.info -> location_files option