aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-21 17:37:10 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-21 17:55:22 +0200
commit1a14ec90521fdeed7db52a59e0a049bf578da487 (patch)
tree28c38f735474b552216b94f2a341d92dfd835f53 /checker
parent18250a35127ed8913dd05f31f109b308a0f11826 (diff)
Adapt checker to change in locations.
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index aec3e3282..a23ca8f4f 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -380,8 +380,10 @@ let init_feedback_listener () =
let pp_loc fmt loc = let open Loc in match loc with
| None -> fprintf fmt ""
| Some loc ->
- fprintf fmt "File \"%s\", line %d, characters %d-%d:@\n"
- loc.fname loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
+ let where =
+ match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in
+ fprintf fmt "\"%s\", line %d, characters %d-%d:@\n"
+ where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
let checker_feed (fb : Feedback.feedback) = let open Feedback in
match fb.contents with
| Processed -> ()