diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-06 11:41:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-14 13:31:27 +0200 |
| commit | 7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa (patch) | |
| tree | 3c0d25c6cb26b5425ec5bc38ed9707c87a8d7e52 /vernac/topfmt.ml | |
| parent | a86bdf0cae05e46d5f0516f29254aeb72bf08de7 (diff) | |
Using an algebraic type for distinguishing toplevel input from location in file.
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e7b14309d..6a10eb43a 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -292,10 +292,11 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in - if CString.equal fname "" then + match fname with + | Loc.ToplevelInput -> Loc.(str"Toplevel input, characters " ++ int loc.bp ++ str"-" ++ int loc.ep ++ str":") - else + | Loc.InFile fname -> Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ str", line " ++ int loc.line_nb ++ str", characters " ++ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ |