diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /vernac/explainErr.ml | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[location] Make location optional in Loc.located
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
Diffstat (limited to 'vernac/explainErr.ml')
| -rw-r--r-- | vernac/explainErr.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index ed2dd274a..040c86805 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -117,8 +117,9 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = try Some (CList.find_map (fun f -> f e) !additional_error_info) with _ -> None in + let add_loc_opt ?loc info = Option.cata (fun l -> Loc.add_loc info l) info loc in match e' with | None -> e - | Some (loc, None) -> (fst e, Loc.add_loc (snd e) loc) + | Some (loc, None) -> (fst e, add_loc_opt ?loc (snd e)) | Some (loc, Some msg) -> - (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc) + (EvaluatedError (msg, Some (fst e)), add_loc_opt ?loc (snd e)) |