Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir

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

4 files changed, 87 insertions, 63 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index f70d67741..8d45151b2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -41,21 +41,11 @@ let load_rcfile() =
     if Options.is_verbose() then mSGNL [< 'sTR"Skipping rcfile loading." >]
 
 let add_ml_include s =
-  Mltop.dir_ml_dir s
+  Mltop.add_ml_dir s
 
 (* Puts dir in the path of ML and in the LoadPath *)
-let add_include s alias =
-  Mltop.dir_ml_dir s;
-  Library.add_path s alias
-
-let add_coq_include s = add_include s [Nametab.coq_root]
-
-let add_rec_include s alias = 
-  let subdirs = all_subdirs s (Some alias) in
-  List.iter (fun lpe -> Mltop.dir_ml_dir lpe.directory) subdirs;
-  List.iter Library.add_load_path_entry subdirs
-
-let add_coq_rec_include s = add_rec_include s [Nametab.coq_root]
+let coq_add_path s = Mltop.add_path s [Nametab.coq_root]
+let coq_add_rec_path s = Mltop.add_rec_path s [Nametab.coq_root]
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -74,26 +64,26 @@ let init_load_path () =
   if Coq_config.local then begin
     (* local use (no installation) *)
     List.iter 
-      (fun s -> add_coq_include (Filename.concat Coq_config.coqtop s))
+      (fun s -> coq_add_path (Filename.concat Coq_config.coqtop s))
       ["states"; "dev"];
-    add_coq_rec_include (Filename.concat Coq_config.coqtop "theories");
-    add_coq_include (Filename.concat Coq_config.coqtop "tactics");
-    add_coq_rec_include (Filename.concat Coq_config.coqtop "contrib")
+    coq_add_rec_path (Filename.concat Coq_config.coqtop "theories");
+    coq_add_path (Filename.concat Coq_config.coqtop "tactics");
+    coq_add_rec_path (Filename.concat Coq_config.coqtop "contrib")
   end else begin
     (* default load path; variable COQLIB overrides the default library *)
     let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
-    add_coq_include (Filename.concat coqlib "states");
-    add_coq_rec_include (Filename.concat coqlib "theories");
-    add_coq_include (Filename.concat coqlib "tactics");
-    add_coq_rec_include (Filename.concat coqlib "contrib")
+    coq_add_path (Filename.concat coqlib "states");
+    coq_add_rec_path (Filename.concat coqlib "theories");
+    coq_add_path (Filename.concat coqlib "tactics");
+    coq_add_rec_path (Filename.concat coqlib "contrib")
   end;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;
-  add_include "." [Nametab.default_root];
+  Mltop.add_path "." [Nametab.default_root];
   (* additional loadpath, given with -I -include -R options *)
   List.iter 
     (fun (s,alias,reci) ->
-       if reci then add_rec_include s alias else add_include s alias)
+       if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
     (List.rev !includes);
   includes := []
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 67fc23a2f..8fd717ff5 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -15,7 +15,7 @@ open Vernacinterp
    \item [dir_ml_load name]: Loads the ML module fname from the current ML 
      path. 
    \item [dir_ml_use]: Directive #use of Ocaml toplevel
-   \item [dir_ml_dir]: Directive #directory of Ocaml toplevel
+   \item [add_ml_dir]: Directive #directory of Ocaml toplevel
    \end{itemize}
  
    How to build an ML module interface with these functions.
@@ -117,15 +117,41 @@ let dir_ml_use s =
     | _ -> warning "Cannot access the ML compiler"
 
 (* Adds a path to the ML paths *)
-let dir_ml_dir s =
+let add_ml_dir s =
   match !load with
     | WithTop t -> t.add_dir s; keep_copy_mlpath s
     | WithoutTop -> keep_copy_mlpath s
     | _ -> ()
 
 (* For Rec Add ML Path *)
-let rdir_ml_dir dir = 
-  List.iter (fun lpe -> dir_ml_dir lpe.directory) (all_subdirs dir None)
+let add_rec_ml_dir dir = 
+  List.iter (fun lpe -> add_ml_dir lpe.directory) (all_subdirs dir None)
+
+(* Adding files to Coq and ML loadpath *)
+
+let add_path dir coq_dirpath =
+  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+  if exists_dir dir then
+    begin
+      add_ml_dir dir;
+      Library.add_load_path_entry
+	{ directory = dir; coq_dirpath = coq_dirpath };
+      Nametab.push_library_root (List.hd coq_dirpath)
+    end
+  else
+    wARNING [< 'sTR ("Cannot open " ^ dir) >]
+
+let add_rec_path dir coq_dirpath =
+  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+  let dirs = all_subdirs dir (Some coq_dirpath) in
+  if dirs <> [] then
+    begin
+      List.iter (fun lpe -> add_ml_dir lpe.directory) dirs;
+      List.iter Library.add_load_path_entry dirs;
+      Nametab.push_library_root (List.hd coq_dirpath)
+    end
+    else
+      wARNING [< 'sTR ("Cannot open " ^ dir) >]
 
 (* convertit un nom quelconque en nom de fichier ou de module *) 
 let mod_of_name name =
@@ -240,41 +266,9 @@ let print_ml_path () =
   pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR"  ";
           hV 0 (prlist_with_sep pr_fnl (fun e -> [< 'sTR e.directory >]) l) >]
 
-let _ = vinterp_add "DeclareMLModule"
-	  (fun l ->
-	     let sl = 
-	       List.map 
-		 (function 
-		    | (VARG_STRING s) -> s 
-		    | _ -> anomaly "DeclareMLModule : not a string") l
-	     in
-    	     fun () -> declare_ml_modules sl)
-	  
-let _ = vinterp_add "AddMLPath"
-	  (function 
-	     | [VARG_STRING s] ->
-		 (fun () -> dir_ml_dir (glob s))
-	     | _ -> anomaly "AddMLPath : not a string")
-
-let _ = vinterp_add "RecAddMLPath"
-	  (function 
-	     | [VARG_STRING s] ->
-		 (fun () -> rdir_ml_dir (glob s))
-	     | _ -> anomaly "RecAddMLPath : not a string")
-
-let _ = vinterp_add "PrintMLPath"
-	  (function 
-	     | [] -> (fun () -> print_ml_path ())
-	     | _ -> anomaly "PrintMLPath : does not expect any argument")
-
 	  (* Printing of loaded ML modules *)
 	  
 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); 'fNL >]
-
-let _ = vinterp_add "PrintMLModules"
-	  (function 
-	     | [] -> (fun () -> print_ml_modules ())
-	     | _ -> anomaly "PrintMLModules : does not expect an argument")
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 467395c1e..b86573c95 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -35,7 +35,12 @@ val dir_ml_load : string -> unit
 val dir_ml_use : string -> unit
 
 (*Adds a path to the ML paths*)
-val dir_ml_dir : string -> unit
+val add_ml_dir : string -> unit
+val add_rec_ml_dir : string -> unit
+
+(*Adds a path to the Coq and ML paths*)
+val add_path : unix_path:string -> coq_root:Names.dir_path -> unit
+val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit
 
 val add_init_with_state : (unit -> unit) -> unit
 val init_with_state : unit -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d8389ac05..9c30cef9a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -32,6 +32,7 @@ open Tacinterp
 open Tactic_debug
 open Command
 open Goptions
+open Mltop
 
 (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *)
 let join_binders binders = 
@@ -197,10 +198,10 @@ let _ =
 	   let alias = Filename.basename dir in
 	   if alias = "" then
 	     error ("Cannot map "^dir^" to a root of Coq library");
-	   (fun () -> rec_add_path dir [alias])
+	   (fun () -> add_rec_path dir [alias])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = repr_qualid alias in
-	    (fun () -> rec_add_path dir (aliasdir@[aliasname]))
+	    (fun () -> add_rec_path dir (aliasdir@[aliasname]))
        | _ -> bad_vernac_args "RECADDPATH")
 
 (* For compatibility *)
@@ -562,7 +563,7 @@ let _ =
   add "SaveNamed"
     (function 
        | [] -> 
-	   (fun () -> if not(is_silent()) then show_script(); save_named true)
+	   (fun () -> if not(is_silent()) then show_script(); save_named false)
        | _ -> bad_vernac_args "SaveNamed")
 
 let _ =
@@ -1738,3 +1739,37 @@ let _ =
 	  if subtree_solved () then 
 	    (reset_top_of_tree (); print_subgoals()) 
        ))
+
+(* Coq syntax for ML commands *)
+
+let _ = vinterp_add "DeclareMLModule"
+	  (fun l ->
+	     let sl = 
+	       List.map 
+		 (function 
+		    | (VARG_STRING s) -> s 
+		    | _ -> anomaly "DeclareMLModule : not a string") l
+	     in
+    	     fun () -> declare_ml_modules sl)
+	  
+let _ = vinterp_add "AddMLPath"
+	  (function 
+	     | [VARG_STRING s] ->
+		 (fun () -> add_ml_dir (glob s))
+	     | _ -> anomaly "AddMLPath : not a string")
+
+let _ = vinterp_add "RecAddMLPath"
+	  (function 
+	     | [VARG_STRING s] ->
+		 (fun () -> add_rec_ml_dir (glob s))
+	     | _ -> anomaly "RecAddMLPath : not a string")
+
+let _ = vinterp_add "PrintMLPath"
+	  (function 
+	     | [] -> (fun () -> print_ml_path ())
+	     | _ -> anomaly "PrintMLPath : does not expect any argument")
+
+let _ = vinterp_add "PrintMLModules"
+	  (function 
+	     | [] -> (fun () -> print_ml_modules ())
+	     | _ -> anomaly "PrintMLModules : does not expect an argument")