aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/db1
-rw-r--r--dev/top_printers.ml4
-rw-r--r--kernel/names.ml19
-rw-r--r--kernel/names.mli7
4 files changed, 24 insertions, 7 deletions
diff --git a/dev/db b/dev/db
index f259b50eb..ece22b3f4 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppexistentialset
install_printer Top_printers.ppintset
install_printer Top_printers.pplab
install_printer Top_printers.ppdir
+install_printer Top_printers.ppmbid
install_printer Top_printers.ppmp
install_printer Top_printers.ppkn
install_printer Top_printers.ppcon
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09..0900bb096 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -40,10 +40,10 @@ let ppid id = pp (pr_id id)
let pplab l = pp (pr_lab l)
let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
let ppdir dir = pp (pr_dirpath dir)
-let ppmp mp = pp(str (string_of_mp mp))
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
let ppcon con = pp(debug_pr_con con)
let ppproj con = pp(debug_pr_con (Projection.constant con))
-let ppkn kn = pp(pr_kn kn)
+let ppkn kn = pp(str (KerName.to_string kn))
let ppmind kn = pp(debug_pr_mind kn)
let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
let ppsp sp = pp(pr_path sp)
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 *)