diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ac9293d5f..972d83055 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -18,14 +18,15 @@ open Vernacexpr Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -(* The navigation vernac commands will be handled separately *) +(* Navigation commands are allowed in a coqtop session but not in a .v file *) let rec is_navigation_vernac = function | VernacResetInitial | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ - | VernacBack _ -> true + | VernacBack _ + | VernacStm _ -> true | VernacRedirect (_, (_,c)) | VernacTime (_,c) -> is_navigation_vernac c (* Time Back* is harmless *) @@ -230,6 +231,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in + CWarnings.set_current_loc (fst loc_ast); vernac_com verbosely checknav loc_ast done with any -> (* whatever the exception *) @@ -272,11 +274,17 @@ let load_vernac verb file = if !Flags.beautify_file then close_out !chan_beautify; iraise (disable_drop e, info) +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") + let ensure_ext ext f = if Filename.check_suffix f ext then f else begin - Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ - expanded to \"" ++ str f ++ str ext ++ str "\""); + warn_file_no_extension (f,ext); f ^ ext end |