modules profile, Coqinit et Coqtop (=main)

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

1 files changed, 28 insertions, 17 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 65bb4f4d8..f6f696ea3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -90,23 +90,34 @@ let just_parsing = ref false
 
 let rec vernac interpfun input =
   let com = parse_phrase input in
-  try
-    match com with
-      | Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
-          let verbosely = verbosely = "Verbose" in
-          raw_load_vernac_file verbosely (make_suffix fname ".v")
-            
-      | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
-                               Str (_,mname); Str(_,fname)]) ->
-          let verbosely = verbosely = "Verbose" in
-          let only_spec = only_spec = "Specification" in
-          States.with_heavy_rollback (* to roll back in case of error *)
-            (raw_compile_module verbosely only_spec mname)
-            (make_suffix fname ".v")
-      | _ -> if not !just_parsing then interpfun com
-  with e -> 
-    raise (DuringCommandInterp (Ast.loc com, e))
-      
+  let rec interp com =
+    try
+      match com with
+	| Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
+            let verbosely = verbosely = "Verbose" in
+            raw_load_vernac_file verbosely (make_suffix fname ".v")
+              
+	| Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
+				 Str (_,mname); Str(_,fname)]) ->
+            let verbosely = verbosely = "Verbose" in
+            let only_spec = only_spec = "Specification" in
+            States.with_heavy_rollback (* to roll back in case of error *)
+              (raw_compile_module verbosely only_spec mname)
+              (make_suffix fname ".v")
+	      
+	| Node(_,"Time",l) ->
+	    let tstart = System.get_time() in
+            List.iter interp l;
+	    let tend = System.get_time() in
+            mSGNL [< 'sTR"Finished transaction in " ;
+                     System.fmt_time_difference tstart tend >]
+	      
+	| _ -> if not !just_parsing then interpfun com
+    with e -> 
+      raise (DuringCommandInterp (Ast.loc com, e))
+  in 
+  interp com
+     
 and raw_load_vernac_file verbosely s =
   let _ = read_vernac_file verbosely s in ()