adds a new command add_rec_path for the parser program and changes add_path

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

3 files changed, 20 insertions, 46 deletions

diff --git a/contrib/interface/line_parser.ml4 b/contrib/interface/line_parser.ml4
index 91eda0eed..b56693512 100755
--- a/contrib/interface/line_parser.ml4
+++ b/contrib/interface/line_parser.ml4
@@ -26,10 +26,10 @@ let add_in_buff,get_buff =
          succ i),
      (fun len -> String.sub !buff 0 len);;
 
-(* Identifiers are [a-zA-Z_][a-zA-Z0-9_]*.  When arriving here the first
+(* Identifiers are [a-zA-Z_][.a-zA-Z0-9_]*.  When arriving here the first
    character has already been recognized. *)
 let rec ident len = parser
-  [<''_' | 'a'..'z' | 'A'..'Z' | '0'..'9' as c; s >] ->
+  [<''_' | '.' | 'a'..'z' | 'A'..'Z' | '0'..'9' as c; s >] ->
     ident (add_in_buff len c) s
 | [< >] -> let str = get_buff len in Tid(str);;
 
@@ -176,6 +176,8 @@ type parser_request =
       (* parse_file <int> <string> *)
   | ADD_PATH of string
       (* add_path <int> <string> *)
+  | ADD_REC_PATH of string * string
+      (* add_rec_path <int> <string> <ident> *)
   | LOAD_SYNTAX of string
       (* load_syntax_file <int> <ident> *)
   | GARBAGE
@@ -190,6 +192,7 @@ let parser_loop functions input_channel =
       quiet_parse_string_action,
       parse_file_action,
       add_path_action,
+      add_rec_path_action,
       load_syntax_action = functions in
   let rec parser_loop_rec input_channel =
   (let line = input_line input_channel in
@@ -206,6 +209,8 @@ let parser_loop functions input_channel =
                      0,QUIET_PARSE_STRING
         | [< 'Tid "parse_file" ; 'Tint reqid ; 'Tstring fname >] ->
                      reqid, PARSE_FILE fname
+        | [< 'Tid "add_rec_path"; 'Tint reqid ; 'Tstring directory ;  'Tid alias >]
+            -> reqid, ADD_REC_PATH(directory, alias)
         | [< 'Tid "add_path"; 'Tint reqid ; 'Tstring directory >]
             -> reqid, ADD_PATH directory
         | [< 'Tid "load_syntax_file"; 'Tint reqid; 'Tid module_name >] ->
@@ -229,6 +234,7 @@ let parser_loop functions input_channel =
    | PARSE_FILE file_name ->
         parse_file_action reqid file_name
    | ADD_PATH path -> add_path_action reqid path
+   | ADD_REC_PATH(path, alias) -> add_rec_path_action reqid path alias
    | LOAD_SYNTAX syn -> load_syntax_action reqid syn
    | GARBAGE -> ());
    parser_loop_rec input_channel in
diff --git a/contrib/interface/line_parser.mli b/contrib/interface/line_parser.mli
index 1fcd42e6f..b0b043c75 100644
--- a/contrib/interface/line_parser.mli
+++ b/contrib/interface/line_parser.mli
@@ -1,5 +1,5 @@
 val parser_loop :
   (unit -> unit) * (int -> string -> char Stream.t -> string list -> 'a) *
   (char Stream.t -> 'b) * (int -> string -> unit) * (int -> string -> unit) *
-  (int -> string -> unit) -> in_channel -> 'c
+  (int -> string -> string -> unit) * (int -> string -> unit) -> in_channel -> 'c
 val flush_until_end_of_stream : 'a Stream.t -> unit
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 3becfa29e..eb574a438 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -1,24 +1,15 @@
 open Util;;
-
 open System;;
-
 open Pp;;
-
 open Libnames;;
-
 open Library;;
-
 open Ascent;;
-
 open Vtp;;
-
 open Xlate;;
-
 open Line_parser;;
-
 open Pcoq;;
-
 open Vernacexpr;;
+open Mltop;;
 
 type parsed_tree =
   | P_cl of ct_COMMAND_LIST
@@ -389,39 +380,17 @@ let parse_file_action reqid file_name =
 		  (str "Error with file" ++ spc () ++ str file_name ++
 		   fnl () ++ Cerrors.explain_exn e));;
 
-(* This function is taken from Mltop.add_path *)
-
-let add_path dir coq_dirpath =
-  if exists_dir dir then
-    begin
-      Library.add_load_path_entry (dir,coq_dirpath)
-    end
-  else
-    msg_warning (str ("Cannot open " ^ dir))
-
-let convert_string d =
-  try Names.id_of_string d
-  with _ -> failwith ("could not convert " ^ d)
-
-let add_rec_path dir coq_dirpath =
-  let dirs = all_subdirs dir in
-  let prefix = Names.repr_dirpath coq_dirpath in
-  if dirs <> [] then
-    let convert_dirs (lp,cp) =
-      (lp,
-       Names.make_dirpath ((List.map convert_string (List.rev cp))@prefix)) in
-    let dirs = map_succeed convert_dirs dirs in
+let add_rec_path_action reqid string_arg ident_arg =
+  let directory_name = glob string_arg in
     begin
-      List.iter Library.add_load_path_entry dirs
-    end
-    else
-      msg_warning (str ("Cannot open " ^ dir));;
+      add_rec_path directory_name (Libnames.dirpath_of_string ident_arg)
+    end;;
+	
 
 let add_path_action reqid string_arg =
   let directory_name = glob string_arg in
-  let alias = Filename.basename directory_name in
     begin
-      add_path directory_name (Names.make_dirpath [Names.id_of_string alias])
+      add_path directory_name Names.empty_dirpath
     end;;
 
 let print_version_action () =
@@ -455,10 +424,10 @@ let coqparser_loop inchan =
  (parser_loop : (unit -> unit) *
                 (int -> string -> char Stream.t -> string list -> unit) *
                 (char Stream.t -> unit) * (int -> string -> unit) *
-                (int -> string -> unit) * (int -> string -> unit) ->
-                in_channel -> unit)
+                (int -> string -> unit) * (int -> string -> string -> unit) *
+                (int -> string -> unit) -> in_channel -> unit)
  (print_version_action, parse_string_action, quiet_parse_string_action, parse_file_action,
- add_path_action, load_syntax_action) inchan;;
+ add_path_action, add_rec_path_action, load_syntax_action) inchan;;
 
 if !Sys.interactive then ()
  else 
@@ -477,8 +446,7 @@ Libobject.relax true;
        add_path (Filename.concat coqdir "tactics")
 	 	 (Names.make_dirpath [Nameops.coq_root]);
        add_rec_path (Filename.concat coqdir "contrib")
-	 (Names.make_dirpath [Nameops.coq_root]);
-       List.iter (fun a -> msgnl (str a)) (get_load_path())
+	 (Names.make_dirpath [Nameops.coq_root])
      end;
 (let vernacrc =
    try