aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/topfmt.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/topfmt.ml')
-rw-r--r--vernac/topfmt.ml5
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) ++