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, 31 insertions, 36 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index cf3d6503d..5e20df358 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -87,53 +87,48 @@ let coqbin =
 
 (** The following only makes sense when executables are running from
     source tree (e.g. during build or in local mode). *)
-let coqroot = 
+let coqroot =
   Filename.dirname coqbin
-    
+
 (** On win32, we add coqbin to the PATH at launch-time (this used to be
     done in a .bat script). *)
 let _ =
-  if String.equal Coq_config.arch "win32" then
+  if Coq_config.arch_is_win32 then
     Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> ""))
 
-(** [reldir instdir testfile oth] checks if [testfile] exists in 
-    the installation directory [instdir] given relatively to 
-    [coqroot]. If this Coq is only locally built, then [testfile]
-    must be found at [coqroot]. 
+(** [check_file_else ~dir ~file oth] checks if [file] exists in
+    the installation directory [dir] given relatively to [coqroot].
+    If this Coq is only locally built, then [file] must be in [coqroot].
     If the check fails, then [oth ()] is evaluated. *)
-let reldir instdir testfile oth =
-  let rpath = if Coq_config.local then [] else instdir in
-  let out = List.fold_left ( / ) coqroot rpath in
-  if Sys.file_exists (out / testfile) then out else oth ()
+let check_file_else ~dir ~file oth =
+  let path = if Coq_config.local then coqroot else coqroot / dir in
+  if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
-  let file = "theories/Init/Prelude.vo" in
-    reldir (if String.equal Coq_config.arch "win32" then ["lib"] else ["lib";"coq"]) file
-      (fun () ->
-        let coqlib = match Coq_config.coqlib with
-          | Some coqlib -> coqlib
-          | None -> coqroot
-        in
-        if Sys.file_exists (coqlib / file) then 
-	  coqlib
-        else 
-	  fail "cannot guess a path for Coq libraries; please use -coqlib option")
-
-let coqlib ~fail =
-  if !Flags.coqlib_spec then 
-    !Flags.coqlib 
-  else if !Flags.boot then 
-    coqroot 
-  else 
-    guess_coqlib fail
+  let prelude = "theories/Init/Prelude.vo" in
+  let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in
+  check_file_else ~dir ~file:prelude
+    (fun () ->
+      let coqlib = match Coq_config.coqlib with
+        | Some coqlib -> coqlib
+        | None -> coqroot
+      in
+      if Sys.file_exists (coqlib / prelude) then coqlib
+      else
+        fail "cannot guess a path for Coq libraries; please use -coqlib option")
+
+(** coqlib is now computed once during coqtop initialization *)
+
+let set_coqlib ~fail =
+  if not !Flags.coqlib_spec then
+    let lib = if !Flags.boot then coqroot else guess_coqlib fail in
+    Flags.coqlib := lib
+
+let coqlib () = !Flags.coqlib
 
 let docdir () =
-  reldir (
-    if String.equal Coq_config.arch "win32" then 
-      ["doc"] 
-    else 
-      ["share";"doc";"coq"]
-  ) "html" (fun () -> Coq_config.docdir)
+  let dir = if Coq_config.arch_is_win32 then "doc" else "share/doc/coq" in
+  check_file_else ~dir ~file:"html" (fun () -> Coq_config.docdir)
 
 let coqpath =
   let coqpath = getenv_else "COQPATH" (fun () -> "") in