From 7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 6 May 2017 11:41:33 +0200
Subject: Using an algebraic type for distinguishing toplevel input from
 location in file.

---
 vernac/topfmt.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'vernac/topfmt.ml')

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) ++
-- 
cgit v1.2.3