modules

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

7 files changed, 87 insertions, 59 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 776864d705..6a0a2e2a98 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -3,6 +3,7 @@
 
 open Pp
 open Util
+open Options
 open Generic
 open Term
 open Constant
@@ -40,7 +41,8 @@ let constant_entry_of_com com =
 
 let definition_body ident n com = 
   let ce = constant_entry_of_com com in
-  declare_constant ident (ce,n)
+  declare_constant ident (ce,n);
+  if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
 let red_constant_entry ce = function
   | None -> ce
@@ -57,11 +59,14 @@ let red_constant_entry ce = function
 let definition_body_red ident n com red_option = 
   let ce = constant_entry_of_com com in
   let ce' = red_constant_entry ce red_option in
-  declare_constant ident (ce',n)
+  declare_constant ident (ce',n);
+  if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
 let syntax_definition ident com =
   let c = raw_constr_of_com Evd.empty (Global.context()) com in 
-  Syntax_def.declare_syntactic_definition ident c
+  Syntax_def.declare_syntactic_definition ident c;
+  if is_verbose() then 
+    message ((string_of_id ident) ^ " is now a syntax macro")
 
 (***TODO
 let abstraction_definition ident arity com =
@@ -158,7 +163,7 @@ let build_mutual lparams lnamearconstrs finite =
     in
     States.unfreeze fs;
     let sp = declare_mind mie in
-    pPNL(minductive_message lrecnames);
+    if is_verbose() then pPNL(minductive_message lrecnames);
     for i = 0 to List.length mispecvec - 1 do
       declare_eliminations sp i
     done
@@ -248,7 +253,7 @@ let build_recursive lnameargsardef =
     in 
     (* declare the recursive definitions *)
     declare 0 lnamerec; 
-    pPNL(recursive_message lnamerec)
+    if is_verbose() then pPNL(recursive_message lnamerec)
   end;
   (* The others are declared as normal definitions *)
   let var_subst id = (id,make_substituend (global_reference CCI id)) in
@@ -313,7 +318,7 @@ let build_corecursive lnameardef =
       | _        -> () 
     in 
     declare 0 lnamerec; 
-    pPNL(corecursive_message lnamerec)
+    if is_verbose() then pPNL(corecursive_message lnamerec)
   end;
   let var_subst id =
     (id,make_substituend (global_reference CCI id)) in
@@ -351,4 +356,6 @@ let build_scheme lnamedepindsort =
         declare (i+1) lf
     | _        -> ()
   in 
-  declare 0 lrecnames; pPNL(recursive_message lrecnames)
+  declare 0 lrecnames; 
+  if is_verbose() then pPNL(recursive_message lrecnames)
+
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 282039d986..01cfeb4e24 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -55,12 +55,10 @@ let require () =
     (List.rev !require_list)
 
 
-(*
- * Parsing of the command line.
+(* Parsing of the command line.
  *
- * We no longer use Arg.parse, in order to use Usage.print_usage to be coherent
- * with launch/coqtop and launch/coqc.
- *)
+ * We no longer use Arg.parse, in order to use share Usage.print_usage 
+ * between coqtop and coqc. *)
 
 let usage () =
   if !batch_mode then
@@ -70,62 +68,75 @@ let usage () =
   flush stderr ;
   exit 1
 
+let version () =
+  Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
+    Coq_config.version Coq_config.date;
+  Printf.printf "compiled on %s\n" Coq_config.compile_date;
+  exit 0
 
 let parse_args () =
   let rec parse = function
     | [] -> ()
 
-    | ("-I"|"-include") :: d :: rem -> push_include d ; parse rem
+    | ("-I"|"-include") :: d :: rem -> push_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | ("-R") :: d :: rem -> rec_include d ; parse rem
-    | ("-R") :: []       -> usage ()
+    | "-R" :: d :: rem -> rec_include d; parse rem
+    | "-R" :: []       -> usage ()
 
-    | "-q" :: rem -> no_load_rc () ; parse rem
+    | "-q" :: rem -> no_load_rc (); parse rem
 
-    | "-batch" :: rem -> set_batch_mode () ; parse rem
+    | "-batch" :: rem -> set_batch_mode (); parse rem
 	     
-    | "-outputstate" :: s :: rem -> set_outputstate s ; parse rem
+    | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()
 
-    | "-nois" :: rem -> set_inputstate "" ; parse rem
+    | "-nois" :: rem -> set_inputstate ""; parse rem
 	     
-    | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s ; parse rem
+    | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
     | ("-inputstate"|"-is") :: []       -> usage ()
 
-    | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f ; parse rem
+    | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
     | "-load-ml-object" :: []       -> usage ()
 
-    | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f ; parse rem
+    | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
     | "-load-ml-source" :: []       -> usage ()
 
-    | "-load-vernac-source" :: f :: rem -> add_load_vernacular f ; parse rem
+    | "-load-vernac-source" :: f :: rem -> add_load_vernacular f; parse rem
     | "-load-vernac-source" :: []       -> usage ()
 
-    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f ; parse rem
+    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
     | "-load-vernac-object" :: []       -> usage ()
 
-    | "-require" :: f :: rem -> add_require f ; parse rem
+    | "-require" :: f :: rem -> add_require f; parse rem
     | "-require" :: []       -> usage ()
 
-    | "-unsafe" :: f :: rem -> add_unsafe f ; parse rem
+    | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
 
-    | "-debug" :: rem -> set_debug () ; parse rem
+    | "-debug" :: rem -> set_debug (); parse rem
 
-    | "-emacs" :: rem -> Printer.print_emacs := true ; parse rem
+    | "-emacs" :: rem -> Printer.print_emacs := true; parse rem
+	  
+    | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
 
-    | "-init-file" :: f :: rem -> set_rcfile f ; parse rem
+    | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem
+
+    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+
+    | ("-v"|"--version") :: _ -> version ()
+
+    | "-init-file" :: f :: rem -> set_rcfile f; parse rem
     | "-init-file" :: []       -> usage ()
 
-    | "-user" :: u :: rem -> set_rcuser u ; parse rem
+    | "-user" :: u :: rem -> set_rcuser u; parse rem
     | "-user" :: []       -> usage ()
 
-    | "-notactics" :: rem -> remove_top_ml () ; parse rem
+    | "-notactics" :: rem -> remove_top_ml (); parse rem
 
-    | "-just-parsing" :: rem -> Vernac.just_parsing := true ; parse rem
+    | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
 
-    | s :: _ -> prerr_endline ("Don't know what to do with " ^ s) ; usage ()
+    | s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage ()
 
   in
   try
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index f0a97c2180..15f52e412b 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -182,11 +182,11 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
 (* Discharge of the various objects of the environment. *)
 
 let constant_message id =
-  if Options.verbose() then 
+  if Options.is_verbose() then 
     pPNL [< print_id id; 'sTR " is discharged." >]
 
 let inductive_message inds =
-  if Options.verbose() then 
+  if Options.is_verbose() then 
     pPNL (hOV 0 
 	    (match inds with
 	       | [] -> assert false
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index af8b7c5cbf..ba1f36cd7c 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -48,9 +48,9 @@ let rec explain_exn_default = function
 
   | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
 
-  | TypeError(k,ctx,te) -> Himsg.explain_type_error k ctx te
+  | TypeError(k,ctx,te) -> hOV 0 (Himsg.explain_type_error k ctx te)
 
-  | InductiveError e -> Himsg.explain_inductive_error e
+  | InductiveError e -> hOV 0 (Himsg.explain_inductive_error e)
 
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index d2a2400754..3135d53fc4 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -263,7 +263,7 @@ let _ = vinterp_add "PrintMLPath"
 let print_ml_modules () =
   let l = get_loaded_modules () in
   pP [< 'sTR"Loaded ML Modules : " ;
-        hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
+        hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l); 'fNL >]
 
 let _ = vinterp_add "PrintMLModules"
 	  (function 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 2c230365df..a87e61bc53 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -9,7 +9,7 @@ let print_usage_channel co command =
   output_string co
 "  -I dir                 add directory dir in the include path
   -include dir           (idem)
-  -R dir                 add recursively dir
+  -R dir                 add dir recursively
   -src                   add source directories in the include path
 
   -inputstate f          read state from file f.coq
@@ -33,8 +33,8 @@ let print_usage_channel co command =
   -v                     print Coq version and exit
 
   -q                     skip loading of rcfile
-  -init-file f           give the rcfile f
-  -user u                give the user u
+  -init-file f           set the rcfile to f
+  -user u                use the rcfile of user u
   -batch                 batch mode (exits just after arguments parsing)
   -emacs                 tells Coq it is executed under Emacs
 "
@@ -46,7 +46,7 @@ let print_usage = print_usage_channel stderr
 let print_usage_coqtop () =
   print_usage "Usage: coqtop <options>\n";
   output_string stderr
-"  -searchisos            run Coq_SearchIsos\n";;
+"  -searchisos            run Coq_SearchIsos\n"
 
 let print_usage_coqc () =
   print_usage "Usage: coqc [-i] [-t] <options> file...\n
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 93a3303165..a50dcfdf50 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -269,10 +269,19 @@ let _ =
   add "BeginModule"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   fun () -> Library.open_module (string_of_id id)
+	   fun () -> Lib.start_module (string_of_id id)
        | _ -> bad_vernac_args "BeginModule")
 
 let _ =
+  add "WriteModule"
+    (function 
+       | [VARG_IDENTIFIER id] ->
+	   fun () -> let m = string_of_id id in Library.save_module_to m m
+       | [VARG_IDENTIFIER id; VARG_STRING f] ->
+	   fun () -> Library.save_module_to (string_of_id id) f
+       | _ -> bad_vernac_args "WriteModule")
+
+let _ =
   add "ReadModule"
     (function 
        | [VARG_IDENTIFIER id] ->
@@ -281,19 +290,27 @@ let _ =
        | _ -> bad_vernac_args "ReadModule")
 
 let _ =
+  add "ImportModule"
+    (function 
+       | [VARG_IDENTIFIER id] ->
+	   fun () -> 
+	     without_mes_ambig Library.open_module (string_of_id id)
+       | _ -> bad_vernac_args "ImportModule")
+
+let _ =
   add "PrintModules"
     (function 
        | [] -> 
 	   (fun () ->
               let opened = Library.opened_modules ()
 	      and loaded = Library.loaded_modules () in
-              mSG [< 'sTR"Imported (open) Modules: " ;
+              mSG [< 'sTR"Loaded Modules: ";
+		     hOV 0 (prlist_with_sep pr_fnl 
+			      (fun s -> [< 'sTR s >]) loaded);
+		     'fNL;
+		     'sTR"Imported (open) Modules: ";
 		     hOV 0 (prlist_with_sep pr_fnl
-			      (fun s -> [< 'sTR s >]) opened) ; 
-		     'fNL ;
-		     'sTR"Loaded Modules: " ;
-		     hOV 0 (prlist_with_sep pr_fnl
-			      (fun s -> [< 'sTR s >]) loaded) ;
+			      (fun s -> [< 'sTR s >]) opened); 
 		     'fNL >])
        | _ -> bad_vernac_args "PrintModules")
 
@@ -733,7 +750,6 @@ let _ =
 	   in 
 	   fun () ->
 	     definition_body_red id stre c red_option;
-	     message ((string_of_id id) ^ " is defined");
              if coe then begin
 	       Class.try_add_new_coercion id stre;
                message ((string_of_id id) ^ " is now a coercion")
@@ -1040,20 +1056,14 @@ let _ =
   add "SyntaxMacro"
     (function 
        | [VARG_IDENTIFIER id;VARG_COMMAND com] ->
-	   (fun () -> 
-	      syntax_definition id com;
-              if not(is_silent()) then
-                message ((string_of_id id) ^ " is now a syntax macro"))
+	   (fun () -> syntax_definition id com)
        | [VARG_IDENTIFIER id;VARG_COMMAND com; VARG_NUMBER n] ->
            (fun () ->
               let rec aux t = function
                 | 0 -> t
-               	| n -> aux (ope("APPLIST",
-                               	[t;ope("ISEVAR",[])])) (n-1)
+               	| n -> aux (ope("APPLIST",[t;ope("ISEVAR",[])])) (n-1)
               in 
-	      syntax_definition id (aux com n);
-              if not(is_silent()) then
-                message ((string_of_id id) ^ " is now a syntax macro"))
+	      syntax_definition id (aux com n))
        | _ -> bad_vernac_args "SyntaxMacro")
 
 (***