option -m (utilisation memoire)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1366 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3d809508b..66c2e0301 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -13,6 +13,14 @@ let print_header () =
   Printf.printf "Welcome to Coq %s (%s)\n" Coq_config.version Coq_config.date;
   flush stdout
 
+let memory_stat = ref false
+
+let print_memory_stat () = 
+  if !memory_stat then
+    Format.printf "memory use = %d kbytes\n" (heap_size_kb ())
+
+let _ = at_exit print_memory_stat
+
 let set_batch_mode () = batch_mode := true
 
 let remove_top_ml () = Mltop.remove ()
@@ -155,6 +163,8 @@ let parse_args () =
 
     | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
 
+    | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem
+
     | s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage ()
 
   in