diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 77 |
1 files changed, 39 insertions, 38 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 176a6c33..a0cd618e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -27,7 +27,7 @@ let rec is_navigation_vernac = function | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true - | VernacTime l -> + | VernacRedirect (_, l) | VernacTime l -> List.exists (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *) | c -> is_deep_navigation_vernac c @@ -78,9 +78,13 @@ 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 raise_with_file f (e, info) = - let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in - iraise (e, add_exn_files info { outer = f; inner = inner_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." @@ -88,28 +92,12 @@ let disable_drop = function let user_error loc s = Errors.user_err_loc (loc,"_",str s) -(* Open an utf-8 encoded file and skip the byte-order mark if any *) - -let open_utf8_file_in fname = - let is_bom s = - Int.equal (Char.code s.[0]) 0xEF && - Int.equal (Char.code s.[1]) 0xBB && - Int.equal (Char.code s.[2]) 0xBF - in - let in_chan = open_in fname in - let s = " " in - if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; - in_chan - (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. Note: we could use only one thanks to seek_in, but seeking on and on in the file we parse seems a bit risky to me. B.B. *) -let open_file_twice_if verbosely fname = - let paths = Loadpath.get_paths () in - let _,longfname = - find_file_in_path ~warn:(Flags.is_verbose()) paths fname in +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 @@ -208,26 +196,24 @@ let display_cmd_header loc com = let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str (" ["^cmd^"] ")); + str " [" ++ str cmd ++ str "] "); Pp.flush_all () -let rec vernac_com verbosely checknav (loc,com) = +let rec vernac_com verbose checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let f = Loadpath.locate_file fname in let st = save_translator_coqdoc () in if !Flags.beautify_file then begin - let paths = Loadpath.get_paths () in - let _,f = find_file_in_path ~warn:(Flags.is_verbose()) - paths - (CUnix.make_suffix fname ".v") in chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] end; begin try - read_vernac_file verbosely (CUnix.make_suffix fname ".v"); + read_vernac_file verbosely f; restore_translator_coqdoc st; with reraise -> let reraise = Errors.push reraise in @@ -237,7 +223,7 @@ let rec vernac_com verbosely checknav (loc,com) = | v when !just_parsing -> () - | v -> Stm.interp verbosely (loc,v) + | v -> Stm.interp verbose (loc,v) in try checknav loc com; @@ -253,13 +239,12 @@ let rec vernac_com verbosely checknav (loc,com) = else iraise (reraise, info) and read_vernac_file verbosely s = - Flags.make_warn verbosely; let checknav loc cmd = if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" in - let (in_chan, fname, input) = - open_file_twice_if verbosely s 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 *) @@ -274,6 +259,7 @@ 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) @@ -296,14 +282,22 @@ let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; try - read_vernac_file verb file; + Flags.silently (read_vernac_file verb) file; if !Flags.beautify_file then close_out !chan_beautify; 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) -(* Compile a vernac file (f is assumed without .v suffix) *) +let ensure_v f = + if Filename.check_suffix f ".v" then f + else begin + msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ + expanded to \"" ++ str f ++ str ".v\""); + f ^ ".v" + end + +(* Compile a vernac file *) let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in @@ -311,7 +305,8 @@ let compile verbosely f = (msg_error (str "There are pending proofs"); flush_all (); exit 1) in match !Flags.compilation_mode with | BuildVo -> - let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in + let long_f_dot_v = ensure_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_v in Stm.set_compilation_hints long_f_dot_v; Aux_file.start_aux_file_for long_f_dot_v; Dumpglob.start_dump_glob long_f_dot_v; @@ -327,7 +322,8 @@ let compile verbosely f = Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () | BuildVio -> - let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in + let long_f_dot_v = ensure_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_v in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_v; let _ = load_vernac verbosely long_f_dot_v in @@ -340,13 +336,18 @@ let compile verbosely f = let open Library in Dumpglob.noglob (); let f = if check_suffix f ".vio" then chop_extension f else f in - let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in + let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in Stm.set_compilation_hints lfdv; let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in - Library.save_library_raw lfdv lib univs proofs + Library.save_library_raw lfdv sum lib univs proofs let compile v f = ignore(CoqworkmgrApi.get 1); 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) +) |