diff options
| author | Enrico Tassi | 2015-05-12 07:46:15 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-05-12 08:20:46 +0200 |
| commit | 0803c2dd715e6493c3e4f865bcf9ca2a16318c55 (patch) | |
| tree | 25c1ebaa81e4940fe132c6ddb2a1b8beb0968f33 | |
| parent | 2a2d418971a019202cdb78fabc7658a543f0886d (diff) | |
STM: process_error_hook set in Vernac where fname is known (fix #4229)
In compiler mode, only vernac.ml knows the current file name.
Stm.process_error_hook moved from Vernacentries to Vernac to
be bale to properly enrich the exception with the current file
name (if any).
| -rw-r--r-- | toplevel/vernac.ml | 19 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
2 files changed, 14 insertions, 6 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 11cb047e09..96daf5075d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -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." @@ -258,8 +262,8 @@ and read_vernac_file verbosely s = 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 *) @@ -350,3 +354,8 @@ let compile v f = 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) +) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4300d5e244..6272625bda 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2164,5 +2164,4 @@ let interp ?(verbosely=true) ?proof (loc,c) = else aux false c let () = Hook.set Stm.interp_hook interp -let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error let () = Hook.set Stm.with_fail_hook with_fail |