Localisation des erreurs d'internalisation des notations de tactiques

dans le module de leur définition.
Error_in_file dans Util et étendu avec possibilité de noms de modules


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 14 insertions, 20 deletions

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 399134d11..cbf9de04f 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -129,12 +129,15 @@ let print_highlight_location ib (bp,ep) =
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file s fname (bp,ep) =
-  let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl () ++
-                   str"File " ++ str ("\""^fname^"\"")) in
+let print_location_in_file s inlibrary fname (bp,ep) =
+  let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
   if (bp,ep) = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
+    if inlibrary then
+      (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
+       str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
+    else
     let ic = open_in fname in
     let rec line_of_pos lin bol cnt =
       if cnt < bp then
@@ -146,7 +149,8 @@ let print_location_in_file s fname (bp,ep) =
     try
       let (line, bol) = line_of_pos 1 0 0 in
       close_in ic;
-      (errstrm ++ str", line " ++ int line ++
+      (errstrm  ++ str"File " ++ str ("\""^fname^"\"") ++
+         str", line " ++ int line ++
          str", characters " ++ Cerrors.print_loc (bp-bol,ep-bol) ++ fnl ())
     with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ()))
 	
@@ -218,8 +222,8 @@ let print_toplevel_error exc =
             (print_highlight_location top_buffer loc, ie)
           else 
 	    ((mt ()) (* print_command_location top_buffer dloc *), ie)
-      | Error_in_file (s, (fname, loc), ie) ->
-          (print_location_in_file s fname loc, ie)
+      | Error_in_file (s, (inlibrary, fname, loc), ie) ->
+          (print_location_in_file s inlibrary fname loc, ie)
       | _ -> 
 	  ((mt ()) (* print_command_location top_buffer dloc *), exc)
   in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1119d59c2..8438e9b02 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -26,11 +26,6 @@ open Ppvernacnew
 
 exception DuringCommandInterp of Util.loc * exn
 
-(* Like Exc_located, but specifies the outermost file read, the filename
-   associated to the location of the error, and the error itself. *)
-
-exception Error_in_file of string * (string * Util.loc) * exn
-
 (* Specifies which file is read. The intermediate file names are
    discarded here. The Drop exception becomes an error. We forget
    if the error ocurred during interpretation or not *)
@@ -43,11 +38,11 @@ let raise_with_file file exc =
   in
   let (inner,inex) =
     match re with
-      | Error_in_file (_, (f,loc), e) when loc <> dummy_loc ->
-          ((f, loc), e)
+      | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
+          ((b, f, loc), e)
       | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
-          ((file, loc), e)
-      | _ -> ((file,cmdloc), re)
+          ((false,file, loc), e)
+      | _ -> ((false,file,cmdloc), re)
   in 
   raise (Error_in_file (file, inner, disable_drop inex))
 
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index ca96d9e49..37279a2d5 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -10,11 +10,6 @@
 
 (* Parsing of vernacular. *)
 
-(* Like [Exc_located], but specifies the outermost file read, the input buffer
-   associated to the location of the error, and the error itself. *)
-
-exception Error_in_file of string * (string * Util.loc) * exn
-
 (* Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)