From 8bba34395e520ac606fc3efd0a875699fe968e69 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Sun, 20 Sep 2015 00:08:35 +0200
Subject: Better debug printers for module paths.

Now distinguishes between bound modules (Top#X) and submodules (Top.X).

Could be useful for the regular printer as well (e.g. in error messages), but I
don't know what the compatibility constraints are, so leaving it as it is for
now.
---
 kernel/names.ml  | 19 ++++++++++++++-----
 kernel/names.mli |  7 +++++++
 2 files changed, 21 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index ae2b3b638..9e4e8cd61 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -204,7 +204,7 @@ struct
     DirPath.to_string p ^ "." ^ s
 
   let debug_to_string (i, s, p) =
-    "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
+    "<"^DirPath.to_string p ^"#" ^ s ^"#"^ string_of_int i^">"
 
   let compare (x : t) (y : t) =
     if x == y then 0
@@ -282,6 +282,11 @@ module ModPath = struct
     | MPbound uid -> MBId.to_string uid
     | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l
 
+  let rec debug_to_string = function
+    | MPfile sl -> DirPath.to_string sl
+    | MPbound uid -> MBId.debug_to_string uid
+    | MPdot (mp,l) -> debug_to_string mp ^ "." ^ Label.to_string l
+
   (** we compare labels first if both are MPdots *)
   let rec compare mp1 mp2 =
     if mp1 == mp2 then 0
@@ -375,12 +380,16 @@ module KerName = struct
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
-  let to_string kn =
+  let to_string_gen mp_to_string kn =
     let dp =
       if DirPath.is_empty kn.dirpath then "."
       else "#" ^ DirPath.to_string kn.dirpath ^ "#"
     in
-    ModPath.to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+    mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+
+  let to_string kn = to_string_gen ModPath.to_string kn
+
+  let debug_to_string kn = to_string_gen ModPath.debug_to_string kn
 
   let print kn = str (to_string kn)
 
@@ -500,9 +509,9 @@ module KerPair = struct
   let print kp = str (to_string kp)
 
   let debug_to_string = function
-    | Same kn -> "(" ^ KerName.to_string kn ^ ")"
+    | Same kn -> "(" ^ KerName.debug_to_string kn ^ ")"
     | Dual (knu,knc) ->
-      "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")"
+      "(" ^ KerName.debug_to_string knu ^ "," ^ KerName.debug_to_string knc ^ ")"
 
   let debug_print kp = str (debug_to_string kp)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 7cc444375..77139f1c3 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -217,6 +217,9 @@ sig
 
   val to_string : t -> string
 
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs information related to debug. *)
+
   val initial : t
   (** Name of the toplevel structure ([= MPfile initial_dir]) *)
 
@@ -244,6 +247,10 @@ sig
 
   (** Display *)
   val to_string : t -> string
+
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs information related to debug. *)
+
   val print : t -> Pp.std_ppcmds
 
   (** Comparisons *)
-- 
cgit v1.2.3