diff options
-rwxr-xr-x | contrib/interface/line_parser.ml4 | 10 | ||||
-rw-r--r-- | contrib/interface/line_parser.mli | 2 | ||||
-rw-r--r-- | contrib/interface/parse.ml | 54 |
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 |