diff options
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 6 | ||||
| -rw-r--r-- | parsing/egrammar.ml | 3 | ||||
| -rw-r--r-- | parsing/egrammar.mli | 5 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 2 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 16 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 13 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 5 |
9 files changed, 33 insertions, 24 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index ac28997d5..71bc09cc2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -214,7 +214,7 @@ let print_toplevel_error exc = let (loc,exc) = match exc with | Stdpp.Exc_located (loc, ie) -> (Some loc),ie - | Error_in_file (s, (fname, loc), ie) -> None, ie + | Error_in_file (s, (_,fname, loc), ie) -> None, ie | _ -> dloc,exc in match exc with diff --git a/lib/util.ml b/lib/util.ml index d80f09062..56d6717e3 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -31,6 +31,11 @@ let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) let join_loc (deb1,_) (_,fin2) = (deb1,fin2) +(* 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 * (bool * string * Util.loc) * exn + (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index 58d5150b7..e4a2ef707 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -41,6 +41,12 @@ val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a val join_loc : loc -> loc -> loc +(* Like [Exc_located], but specifies the outermost file read, the + input buffer associated to the location of the error (or the module name + if boolean is true), and the error itself. *) + +exception Error_in_file of string * (bool * string * loc) * exn + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 5880c0263..25333b684 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -26,7 +26,8 @@ type all_grammar_command = int list option) | Grammar of grammar_command | TacticGrammar of - (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) + (string * (string * grammar_production list) * + (Names.dir_path * Tacexpr.raw_tactic_expr)) list let subst_all_grammar_command subst = function diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e1f4dc6b1..47b8beced 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -22,7 +22,10 @@ type all_grammar_command = (int * Gramext.g_assoc option * notation * prod_item list * int list option) | Grammar of grammar_command - | TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list + | TacticGrammar of + (string * (string * grammar_production list) * + (Names.dir_path * Tacexpr.raw_tactic_expr)) + list val extend_grammar : all_grammar_command -> unit diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index cf4741e5e..c55fc31a8 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -192,7 +192,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* For syntax extensions *) | TacAlias of loc * string * (identifier * ('constr,'tac) generic_argument) list - * 'tac + * (dir_path * 'tac) and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr 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. *) |