From b847fcc99e35a09b862aa758c5e3f0b08a93202d Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 12 Feb 2004 19:35:23 +0000 Subject: 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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/toplevel.ml | 16 ++++++++++------ toplevel/vernac.ml | 13 ++++--------- toplevel/vernac.mli | 5 ----- 3 files changed, 14 insertions(+), 20 deletions(-) (limited to 'toplevel') 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. *) -- cgit v1.2.3