Merge remote-tracking branch 'github/pr/212' into trunk

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 9c3b170b9..ac9293d5f 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
@@ -389,8 +369,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