Misc changes around coqtop.ml :

 - Revised Coqtop.parse_args in a cleaner and lighter style
 - Improved error message in case of argument parse failure:
   * tell which option is expecting a related argument
   * in case of unknown options, warn about them all at once
   * do not hide the previous error messages by filling the
     screen with usage(). Instead, suggest the use of --help.
 - Specialized boolean config field Coq_config.arch_is_win32
 - Faster Envars.coqlib, which is back to (unit->string), and
   just access Flags.coqlib. Caveat: it must be initialized once
   via Envars.set_coqlib
 - Avoid keeping an opened channel to the "revision" file
 - Direct load of theories/init/prelude.vo, no detour via Loadpath

Beware : ./configure must be runned after this commit

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

1 files changed, 11 insertions, 8 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 280f34656..d54e9328a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -42,21 +42,21 @@ let path_of_string s =
       [] -> invalid_arg "path_of_string"
     | l::dir -> {dirpath=dir; basename=l}
 
-let (/) = Filename.concat
+let ( / ) = Filename.concat
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib error in
-    let ch = open_in (Filename.concat coqlib "revision") in
+    let ch = open_in (Envars.coqlib () / "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
-      (ver,rev)
+    let () = close_in ch in
+    (ver,rev)
   with _ -> (Coq_config.version,Coq_config.date)
 
 let print_header () =
   let (ver,rev) = (get_version_date ()) in
-    Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
-    flush stdout
+  Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
+  flush stdout
 
 (* Adding files to Coq loadpath *)
 
@@ -107,7 +107,7 @@ let set_rec_include d p =
 
 (* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib = Envars.coqlib error in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs in
   let coqpath = Envars.coqpath in
@@ -306,7 +306,9 @@ let parse_args argv =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        print_endline (Envars.coqlib error); exit 0
+        Envars.set_coqlib ~fail:Errors.error;
+        print_endline (Envars.coqlib ());
+        exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
@@ -341,6 +343,7 @@ let init_with_argv argv =
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
     try
       parse_args argv;
+      Envars.set_coqlib ~fail:Errors.error;
       if_verbose print_header ();
       init_load_path ();
       engage ();