diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/config_lexer.mll | 7 | ||||
-rw-r--r-- | ide/coqide.ml | 32 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 4 | ||||
-rw-r--r-- | ide/coqide_ui.ml | 2 | ||||
-rw-r--r-- | ide/ideproof.ml | 2 | ||||
-rw-r--r-- | ide/ideutils.ml | 34 | ||||
-rw-r--r-- | ide/ideutils.mli | 13 | ||||
-rw-r--r-- | ide/minilib.ml | 168 | ||||
-rw-r--r-- | ide/minilib.mli | 32 | ||||
-rw-r--r-- | ide/preferences.ml | 24 | ||||
-rw-r--r-- | ide/project_file.ml4 | 32 | ||||
-rw-r--r-- | ide/utils/configwin_messages.ml | 2 | ||||
-rw-r--r-- | ide/wg_Command.ml | 2 | ||||
-rw-r--r-- | ide/wg_Notebook.ml | 12 |
14 files changed, 67 insertions, 299 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 57699c686..fe790042b 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -10,7 +10,6 @@ open Lexing open Format - open Minilib let string_buffer = Buffer.create 1024 @@ -23,7 +22,7 @@ let ignore = space | ('#' [^ '\n']*) rule prefs m = parse |ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in - prefs (Stringmap.add id conf m) lexbuf } + prefs (Util.Stringmap.add id conf m) lexbuf } | _ { let c = lexeme_start lexbuf in eprintf "coqiderc: invalid character (%d)\n@." c; prefs m lexbuf } @@ -48,7 +47,7 @@ and string = parse let load_file f = let c = open_in f in let lb = from_channel c in - let m = prefs Stringmap.empty lb in + let m = prefs Util.Stringmap.empty lb in close_in c; m @@ -59,7 +58,7 @@ and string = parse | [] -> () | s :: sl -> fprintf fmt "%S@ %a" s print_list sl in - Stringmap.iter + Util.Stringmap.iter (fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m; fprintf fmt "@."; close_out c diff --git a/ide/coqide.ml b/ide/coqide.ml index f44b8a5e3..6e3c85d47 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1419,7 +1419,7 @@ let do_print session = let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in let callback_print () = let cmd = print_entry#text in - let s,_ = run_command av#insert_message cmd in + let s,_ = CUnix.run_command Ideutils.try_convert av#insert_message cmd in flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); print_window#destroy () in @@ -1429,11 +1429,11 @@ let do_print session = end let load_file handler f = - let f = absolute_filename f in + let f = CUnix.correct_path f (Sys.getcwd ()) in try prerr_endline "Loading file starts"; - let is_f = Minilib.same_file f in - if not (Minilib.list_fold_left_i + let is_f = CUnix.same_file f in + if not (Util.list_fold_left_i (fun i found x -> if found then found else let {analyzed_view=av} = x in (match av#filename with @@ -1549,7 +1549,7 @@ let main files = (try let icon_image = Filename.concat (List.find (fun x -> Sys.file_exists (Filename.concat x "coq.png")) - Minilib.xdg_data_dirs) "coq.png" in + (Envars.xdg_data_dirs Ideutils.flash_info)) "coq.png" in let icon = GdkPixbuf.from_file icon_image in w#set_icon (Some icon) with _ -> ()); @@ -1650,7 +1650,7 @@ let main files = local_cd f ^ current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) in - let s,_ = run_command av#insert_message cmd in + let s,_ = CUnix.run_command Ideutils.try_convert av#insert_message cmd in flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" @@ -1769,7 +1769,7 @@ let main files = let cmd = current.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f)) ^ " " ^ (Filename.quote f) in - let s,res = run_command av#insert_message cmd in + let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in if s = Unix.WEXITED 0 then flash_info (f ^ " successfully compiled") else begin @@ -1792,7 +1792,7 @@ let main files = save_f (); *) av#insert_message "Command output:\n"; - let s,res = run_command av#insert_message cmd in + let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in last_make := res; last_make_index := 0; flash_info (current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") @@ -1839,7 +1839,7 @@ let main files = flash_info "Cannot make makefile: this buffer has no name" | Some f -> let cmd = local_cd f ^ current.cmd_coqmakefile in - let s,res = run_command av#insert_message cmd in + let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in flash_info (current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in @@ -1856,7 +1856,7 @@ let main files = let windows_actions = GAction.action_group ~name:"Windows" () in let help_actions = GAction.action_group ~name:"Help" () in let add_gen_actions menu_name act_grp l = - let no_under = Minilib.string_map (fun x -> if x = '_' then '-' else x) in + let no_under = Util.string_map (fun x -> if x = '_' then '-' else x) in let add_simple_template menu_name act_grp text = let text' = let l = String.length text - 1 in @@ -1975,8 +1975,8 @@ let main files = | None -> warning "Call to external editor available only on named files" | Some f -> save_f (); - let com = Minilib.subst_command_placeholder current.cmd_editor (Filename.quote f) in - let _ = run_command av#insert_message com in + let com = Util.subst_command_placeholder current.cmd_editor (Filename.quote f) in + let _ = CUnix.run_command Ideutils.try_convert av#insert_message com in av#revert) ~stock:`EDIT; GAction.add_action "Preferences" ~callback:(fun _ -> begin @@ -2272,7 +2272,7 @@ let main files = (try let image = Filename.concat (List.find (fun x -> Sys.file_exists (Filename.concat x "coq.png")) - Minilib.xdg_data_dirs) "coq.png" in + (Envars.xdg_data_dirs Ideutils.flash_info)) "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; @@ -2284,7 +2284,7 @@ let main files = (try let image = Filename.concat (List.find (fun x -> Sys.file_exists (Filename.concat x "coq.png")) - Minilib.xdg_data_dirs) "coq.png" in + (Envars.xdg_data_dirs Ideutils.flash_info)) "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; @@ -2367,11 +2367,11 @@ let read_coqide_args argv = (output_string stderr "Error: multiple -coqtop options"; exit 1) | "-f" :: file :: args -> filter_coqtop coqtop - ((Minilib.canonical_path_name (Filename.dirname file), + ((CUnix.canonical_path_name (Filename.dirname file), Project_file.read_project_file file) :: project_files) out args | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 | "-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1 - | "-debug"::args -> Ideutils.debug := true; + | "-debug"::args -> Minilib.debug := true; filter_coqtop coqtop project_files ("-debug"::out) args | arg::args -> filter_coqtop coqtop project_files (arg::out) args | [] -> (coqtop,List.rev project_files,List.rev out) diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 4c546ab7f..2dbb3f499 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -34,7 +34,7 @@ let set_win32_path () = let reroute_stdout_stderr () = let out_descr = - if !Ideutils.debug then + if !Minilib.debug then Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log")) else snd (Unix.pipe ()) @@ -97,7 +97,7 @@ let () = try GtkThread.main () with - | Sys.Break -> Ideutils.prerr_endline "Interrupted." + | Sys.Break -> Minilib.prerr_endline "Interrupted." | e -> Minilib.safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 4ba378b7b..04e1e488d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -1,6 +1,6 @@ let ui_m = GAction.ui_manager ();; -let no_under = Minilib.string_map (fun x -> if x = '_' then '-' else x) +let no_under = Util.string_map (fun x -> if x = '_' then '-' else x) let list_items menu li = let res_buf = Buffer.create 500 in diff --git a/ide/ideproof.ml b/ide/ideproof.ml index cfbeec0b2..569e503c3 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -91,7 +91,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with proof#buffer#insert (goal_str i goals_cnt); proof#buffer#insert (g ^ "\n") in - let () = Minilib.list_fold_left_i fold_goal 2 () rem_goals in + let () = Util.list_fold_left_i fold_goal 2 () rem_goals in ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 1eb8a41be..3f9bb3aca 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -29,15 +29,8 @@ let set_location = ref (function s -> failwith "not ready") let pbar = GRange.progress_bar ~pulse_step:0.2 () -let debug = ref (false) - -let prerr_endline s = - if !debug then try prerr_endline s;flush stderr with _ -> () - let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT -let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0 - let byte_offset_to_char_offset s byte_offset = if (byte_offset < String.length s) then begin let count_delta = ref 0 in @@ -282,29 +275,8 @@ let rec print_list print fmt = function let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd -(* TODO: allow to report output as soon as it comes (user-fiendlier - for long commands like make...) *) -let run_command f c = - let c = requote c in - let result = Buffer.create 127 in - let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in - let buff = String.make 127 ' ' in - let buffe = String.make 127 ' ' in - let n = ref 0 in - let ne = ref 0 in - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0 - do - let r = try_convert (String.sub buff 0 !n) in - f r; - Buffer.add_string result r; - let r = try_convert (String.sub buffe 0 !ne) in - f r; - Buffer.add_string result r - done; - (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) - let browse f url = - let com = Minilib.subst_command_placeholder current.cmd_browse url in + let com = Util.subst_command_placeholder current.cmd_browse url in let _ = Unix.open_process_out com in () (* This beautiful message will wait for twt ... if s = 127 then @@ -324,7 +296,7 @@ let url_for_keyword = let cin = try let index_urls = Filename.concat (List.find (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt")) - Minilib.xdg_config_dirs) "index_urls.txt" in + (Envars.xdg_config_dirs flash_info)) "index_urls.txt" in open_in index_urls with Not_found -> let doc_url = doc_url () in @@ -353,5 +325,3 @@ let url_for_keyword = let browse_keyword f text = try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) with Not_found -> f ("No documentation found for \""^text^"\".\n") - -let absolute_filename f = Minilib.correct_path f (Sys.getcwd ()) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index c433d92ac..5aa615549 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -16,7 +16,6 @@ val doc_url : unit -> string val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int -val debug : bool ref val disconnect_revert_timer : unit -> unit val disconnect_auto_save_timer : unit -> unit val do_convert : string -> string @@ -25,13 +24,8 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a -val is_char_start : char -> bool - val my_stat : string -> Unix.stats option -(** debug printing *) -val prerr_endline : string -> unit - val print_id : 'a -> unit val revert_timer : GMain.Timeout.id option ref @@ -50,8 +44,6 @@ val stock_to_widget : ?size:Gtk.Tags.icon_size -> GtkStock.id -> GObj.widget open Format val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit -val run_command : (string -> unit) -> string -> Unix.process_status*string - val custom_coqtop : string option ref (* @return command to call coqtop - custom_coqtop if set @@ -69,11 +61,6 @@ val set_location : (string -> unit) ref val pbar : GRange.progress_bar -(* - returns an absolute filename equivalent to given filename -*) -val absolute_filename : string -> string - (* In win32, when a command-line is to be executed via cmd.exe (i.e. Sys.command, Unix.open_process, ...), it cannot contain several quoted "..." zones otherwise some quotes are lost. Solution: we re-quote diff --git a/ide/minilib.ml b/ide/minilib.ml index 74a42b234..5638934bd 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -9,109 +9,10 @@ (** Some excerpt of Util and similar files to avoid loading the whole module and its dependencies (and hence Compat and Camlp4) *) -module Stringmap = Map.Make(String) +let debug = ref (false) -let list_fold_left_i f = - let rec it_list_f i a = function - | [] -> a - | b::l -> it_list_f (i+1) (f i a b) l - in - it_list_f - -(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that - [l1++l2=l] and [l1] has length [i]. - It raises [Failure] when [i] is negative or greater than the length of [l] *) - -let list_chop n l = - let rec chop_aux i acc = function - | tl when i=0 -> (List.rev acc, tl) - | h::t -> chop_aux (pred i) (h::acc) t - | [] -> failwith "list_chop" - in - chop_aux n [] l - - -let list_map_i f = - let rec map_i_rec i = function - | [] -> [] - | x::l -> let v = f i x in v :: map_i_rec (i+1) l - in - map_i_rec - - -let list_index x = - let rec index_x n = function - | y::l -> if x = y then n else index_x (succ n) l - | [] -> raise Not_found - in - index_x 1 - -let list_index0 x l = list_index x l - 1 - -let list_filter_i p = - let rec filter_i_rec i = function - | [] -> [] - | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l' - in - filter_i_rec 0 - -let string_map f s = - let l = String.length s in - let r = String.create l in - for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done; - r - -let subst_command_placeholder s t = - Str.global_replace (Str.regexp_string "%s") t s - -(* Split the content of a variable such as $PATH in a list of directories. - The separators are either ":" in unix or ";" in win32 *) - -let path_to_list = Str.split (Str.regexp "[:;]") - -(* On win32, the home directory is probably not in $HOME, but in - some other environment variable *) - -let home = - try Sys.getenv "HOME" with Not_found -> - try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> - try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name - -let opt2list = function None -> [] | Some x -> [x] - -let (/) = Filename.concat - -let coqify d = d / "coq" - -let xdg_config_home = - coqify (try Sys.getenv "XDG_CONFIG_HOME" with Not_found -> home / ".config") - -let relative_base = - Filename.dirname (Filename.dirname Sys.executable_name) - -let xdg_config_dirs = - let sys_dirs = - try List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS")) - with - | Not_found when Sys.os_type = "Win32" -> [relative_base / "config"] - | Not_found -> ["/etc/xdg/coq"] - in - xdg_config_home :: sys_dirs @ opt2list Coq_config.configdir - -let xdg_data_home = - coqify - (try Sys.getenv "XDG_DATA_HOME" with Not_found -> home / ".local" / "share") - -let xdg_data_dirs = - let sys_dirs = - try List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS")) - with - | Not_found when Sys.os_type = "Win32" -> [relative_base / "share"] - | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"] - in - xdg_data_home :: sys_dirs @ opt2list Coq_config.datadir - -let coqtop_path = ref "" +let prerr_endline s = + if !debug then try prerr_endline s;flush stderr with _ -> () (* On a Win32 application with no console, writing to stderr raise a Sys_error "bad file descriptor", hence the "try" below. @@ -121,66 +22,3 @@ let coqtop_path = ref "" let safe_prerr_endline s = try prerr_endline s;flush stderr with _ -> () - -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - let l = String.length p in - if l > n && String.sub p 0 n = curdir then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - let l = String.length p in - if l > n && String.sub p 0 n = cwd then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p - -let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f - -(* - checks if two file names refer to the same (existing) file by - comparing their device and inode. - It seems that under Windows, inode is always 0, so we cannot - accurately check if - -*) -(* Optimised for partial application (in case many candidates must be - compared to f1). *) -let same_file f1 = - try - let s1 = Unix.stat f1 in - (fun f2 -> - try - let s2 = Unix.stat f2 in - s1.Unix.st_dev = s2.Unix.st_dev && - if Sys.os_type = "Win32" then f1 = f2 - else s1.Unix.st_ino = s2.Unix.st_ino - with - Unix.Unix_error _ -> false) - with - Unix.Unix_error _ -> (fun _ -> false) diff --git a/ide/minilib.mli b/ide/minilib.mli index 53d6c87c2..1254f5a6d 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -9,36 +9,10 @@ (** Some excerpts of Util and similar files to avoid depending on them and hence on Compat and Camlp4 *) -module Stringmap : Map.S with type key = string - -val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a -val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list -val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list -val list_chop : int -> 'a list -> 'a list * 'a list -val list_index0 : 'a -> 'a list -> int - -val string_map : (char -> char) -> string -> string - -val subst_command_placeholder : string -> string -> string - -val home : string -val xdg_config_home : string -val xdg_config_dirs : string list -val xdg_data_home : string -val xdg_data_dirs : string list - -val coqtop_path : string ref +(** debug printing *) +val debug : bool ref +val prerr_endline : string -> unit (** safe version of Pervasives.prerr_endline (avoid exception in win32 without console) *) val safe_prerr_endline : string -> unit - -val remove_path_dot : string -> string -val strip_path : string -> string -val canonical_path_name : string -> string -(** correct_path f dir = dir/f if f is relative *) -val correct_path : string -> string -> string - -(** checks if two file names refer to the same (existing) file *) -val same_file : string -> string -> bool - diff --git a/ide/preferences.ml b/ide/preferences.ml index d54bb55d3..27245dd00 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -9,28 +9,28 @@ open Configwin open Printf -let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc" -let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys" +let pref_file = Filename.concat (Envars.xdg_config_home Minilib.prerr_endline) "coqiderc" +let accel_file = Filename.concat (Envars.xdg_config_home Minilib.prerr_endline) "coqide.keys" let lang_manager = GSourceView2.source_language_manager ~default:true let () = lang_manager#set_search_path - (Minilib.xdg_data_dirs@lang_manager#search_path) + ((Envars.xdg_data_dirs Minilib.prerr_endline)@lang_manager#search_path) let style_manager = GSourceView2.source_style_scheme_manager ~default:true let () = style_manager#set_search_path - (Minilib.xdg_data_dirs@style_manager#search_path) + ((Envars.xdg_data_dirs Minilib.prerr_endline)@style_manager#search_path) let get_config_file name = let find_config dir = Sys.file_exists (Filename.concat dir name) in - let config_dir = List.find find_config Minilib.xdg_config_dirs in + let config_dir = List.find find_config (Envars.xdg_config_dirs Minilib.prerr_endline) in Filename.concat config_dir name (* Small hack to handle v8.3 to v8.4 change in configuration file *) let loaded_pref_file = try get_config_file "coqiderc" - with Not_found -> Filename.concat Minilib.home ".coqiderc" + with Not_found -> Filename.concat (Envars.home Minilib.prerr_endline) ".coqiderc" let loaded_accel_file = try get_config_file "coqide.keys" - with Not_found -> Filename.concat Minilib.home ".coqide.keys" + with Not_found -> Filename.concat (Envars.home Minilib.prerr_endline) ".coqide.keys" let mod_to_str (m:Gdk.Tags.modifier) = match m with @@ -223,14 +223,14 @@ let current = { } let save_pref () = - if not (Sys.file_exists Minilib.xdg_config_home) - then Unix.mkdir Minilib.xdg_config_home 0o700; + if not (Sys.file_exists (Envars.xdg_config_home Minilib.prerr_endline)) + then Unix.mkdir (Envars.xdg_config_home Minilib.prerr_endline) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in let p = current in - let add = Minilib.Stringmap.add in + let add = Util.Stringmap.add in let (++) x f = f x in - Minilib.Stringmap.empty ++ + Util.Stringmap.empty ++ add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++ add "cmd_coqc" [p.cmd_coqc] ++ add "cmd_make" [p.cmd_make] ++ @@ -292,7 +292,7 @@ let load_pref () = let m = Config_lexer.load_file loaded_pref_file in let np = current in - let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in + let set k f = try let v = Util.Stringmap.find k m in f v with _ -> () in let set_hd k f = set k (fun v -> f (List.hd v)) in let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in let set_int k f = set_hd k (fun v -> f (int_of_string v)) in diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 6bee0fec1..0a2720c46 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -72,13 +72,13 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) | "-custom" :: com :: dependencies :: file :: r -> process_cmd_line orig_dir opts (Special (file,dependencies,com) :: l) r | "-I" :: d :: r -> - process_cmd_line orig_dir opts ((Include (Minilib.correct_path d orig_dir)) :: l) r + process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir)) :: l) r | "-R" :: p :: lp :: r -> - process_cmd_line orig_dir opts (RInclude (Minilib.correct_path p orig_dir,lp) :: l) r + process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r | ("-I"|"-custom") :: _ -> raise Parsing_error | "-f" :: file :: r -> - let file = Minilib.remove_path_dot (Minilib.correct_path file orig_dir) in + let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match project_file with | None -> () | Some _ -> Minilib.safe_prerr_endline @@ -104,7 +104,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) | "-arg" :: a :: r -> process_cmd_line orig_dir opts (Arg a :: l) r | f :: r -> - let f = Minilib.correct_path f orig_dir in + let f = CUnix.correct_path f orig_dir in process_cmd_line orig_dir opts (( if Filename.check_suffix f ".v" then V f else if (Filename.check_suffix f ".ml") then ML f @@ -124,32 +124,32 @@ let rec post_canonize f = let split_arguments = let rec aux = function | V n :: r -> - let (v,m,o,s),i,d = aux r in ((Minilib.remove_path_dot n::v,m,o,s),i,d) + let (v,m,o,s),i,d = aux r in ((CUnix.remove_path_dot n::v,m,o,s),i,d) | ML n :: r -> let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,ml4,Minilib.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) + ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) | MLI n :: r -> let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(Minilib.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) + ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) | ML4 n :: r -> let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,Minilib.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) + ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) | MLLIB n :: r -> let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,ml4,ml,Minilib.remove_path_dot n::mllib,mlpack),o,s),i,d) + ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) | MLPACK n :: r -> let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,ml4,ml,mllib,Minilib.remove_path_dot n::mlpack),o,s),i,d) + ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) | Special (n,dep,c) :: r -> let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,c)::o,s),i,d) | Subdir n :: r -> let (v,m,o,s),i,d = aux r in ((v,m,o,n::s),i,d) | Include p :: r -> - let t,(i,r),d = aux r in (t,((Minilib.remove_path_dot (post_canonize p), - Minilib.canonical_path_name p)::i,r),d) + let t,(i,r),d = aux r in (t,((CUnix.remove_path_dot (post_canonize p), + CUnix.canonical_path_name p)::i,r),d) | RInclude (p,l) :: r -> - let t,(i,r),d = aux r in (t,(i,(Minilib.remove_path_dot (post_canonize p),l, - Minilib.canonical_path_name p)::r),d) + let t,(i,r),d = aux r in (t,(i,(CUnix.remove_path_dot (post_canonize p),l, + CUnix.canonical_path_name p)::r),d) | Def (v,def) :: r -> let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs)) | Arg a :: r -> @@ -162,9 +162,9 @@ let read_project_file f = (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) let args_from_project file project_files default_name = - let is_f = Minilib.same_file file in + let is_f = CUnix.same_file file in let contains_file dir = - List.exists (fun x -> is_f (Minilib.correct_path x dir)) + List.exists (fun x -> is_f (CUnix.correct_path x dir)) in let build_cmd_line i_inc r_inc args = List.fold_right (fun (_,i) o -> "-I" :: i :: o) i_inc diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml index de2924318..6cd3ef579 100644 --- a/ide/utils/configwin_messages.ml +++ b/ide/utils/configwin_messages.ml @@ -30,7 +30,7 @@ let version = "1.2";; let html_config = "Configwin bindings configurator for html parameters" -let home = Minilib.home +let home = Envars.home ~warn:Minilib.prerr_endline let mCapture = "Capture";; let mType_key = "Type key" ;; diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index e15e1960b..9d1951851 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -55,7 +55,7 @@ class command_window coqtop = let remove_cb () = let index = notebook#current_page in let () = notebook#remove_page index in - views := Minilib.list_filter_i (fun i x -> i <> index) !views + views := Util.list_filter_i (fun i x -> i <> index) !views in let _ = toolbar#insert_button diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml index 499d56bd9..048cc6e24 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.ml @@ -16,14 +16,14 @@ object(self) (* XXX - Temporary hack to compile with archaic lablgtk *) ignore (super#append_page ?tab_label ?menu_label page); let real_pos = super#page_num page in - let lower,higher = Minilib.list_chop real_pos term_list in + let lower,higher = Util.list_chop real_pos term_list in term_list <- lower@[term]@higher; real_pos (* XXX - Temporary hack to compile with archaic lablgtk method insert_term ?(build=default_build) ?pos (term:'a) = let tab_label,menu_label,page = build term in let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in - let lower,higher = Minilib.list_chop real_pos term_list in + let lower,higher = Util.list_chop real_pos term_list in term_list <- lower@[term]@higher; real_pos *) @@ -32,26 +32,26 @@ object(self) (* XXX - Temporary hack to compile with archaic lablgtk *) ignore (super#prepend_page ?tab_label ?menu_label page); let real_pos = super#page_num page in - let lower,higher = Minilib.list_chop real_pos term_list in + let lower,higher = Util.list_chop real_pos term_list in term_list <- lower@[term]@higher; real_pos method set_term (term:'a) = let tab_label,menu_label,page = make_page term in let real_pos = super#current_page in - term_list <- Minilib.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list; + term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list; super#set_page ?tab_label ?menu_label page method get_nth_term i = List.nth term_list i method term_num p = - Minilib.list_index0 p term_list + Util.list_index0 p term_list method pages = term_list method remove_page index = - term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list; + term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list; super#remove_page index method current_term = |