From 6b2d99445d35ea71cd24becb7f936e0cc9779d46 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 8 Feb 2001 08:29:12 +0000
Subject: simplification du make depend; fonctions de stat. util. memoire dans
 certains modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/library.ml  | 10 ++++++++++
 library/library.mli |  4 ++++
 2 files changed, 14 insertions(+)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 6ff8a84db1..b0c1a2ecd0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -249,3 +249,13 @@ let fmt_modules_state () =
      prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
      'sTR "Loaded Modules: " ;
      prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
+
+(*s Display the memory use of a module. *)
+
+open Printf
+
+let mem s =
+  let m = find_module s in
+  h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk / nmt = %dk)"
+		 (size_kb m) (size_kb m.module_compiled_env) 
+		 (size_kb m.module_declarations) (size_kb m.module_nametab)) >]
diff --git a/library/library.mli b/library/library.mli
index 18ebb97088..43fa04e8bf 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -59,3 +59,7 @@ val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit
 val get_load_path : unit -> System.load_path
 val add_load_path_entry : System.load_path_entry -> unit
 val remove_path : string -> unit
+
+(*s Displays the memory use of a module. *)
+
+val mem : string -> Pp.std_ppcmds
-- 
cgit v1.2.3