Imported Upstream version 8.5~beta1+dfsg

1 files changed, 51 insertions, 167 deletions

diff --git a/ide/minilib.ml b/ide/minilib.ml
index 74a42b23..d11e8c56 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -6,112 +6,23 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+let rec print_list print fmt = function
+  | [] -> ()
+  | [x] -> print fmt x
+  | x :: r -> print fmt x; print_list print fmt r
+
+type level = [
+  | `DEBUG
+  | `INFO
+  | `NOTICE
+  | `WARNING
+  | `ERROR
+  | `FATAL ]
+
 (** 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 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 debug = ref false
 
 (* On a Win32 application with no console, writing to stderr raise
    a Sys_error "bad file descriptor", hence the "try" below.
@@ -119,68 +30,41 @@ let coqtop_path = ref ""
    print in the response buffer.
 *)
 
-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
+let log ?(level = `DEBUG) msg =
+  let prefix = match level with
+  | `DEBUG -> "DEBUG"
+  | `INFO -> "INFO"
+  | `NOTICE -> "NOTICE"
+  | `WARNING -> "WARNING"
+  | `ERROR -> "ERROR"
+  | `FATAL -> "FATAL"
+  in
+  if !debug then begin
+    try Printf.eprintf "[%s] %s\n%!" prefix msg
+    with _ -> ()
+  end
+
+let coqify d = Filename.concat d "coq"
+
+let coqide_config_home () =
+  coqify (Glib.get_user_config_dir ())
+
+let coqide_data_dirs () =
+  coqify (Glib.get_user_data_dir ())
+  :: List.map coqify (Glib.get_system_data_dirs ())
+  @ Option.List.cons Coq_config.datadir []
+
+let coqide_config_dirs () =
+  coqide_config_home ()
+  :: List.map coqify (Glib.get_system_config_dirs ())
+  @ Option.List.cons Coq_config.configdir []
+
+let is_prefix_of pre s =
+  let i = ref 0 in
+  let () = while (!i < (String.length pre)
+        && !i < (String.length s)
+	     && pre.[!i] = s.[!i]) do
+	          incr i
+		     done
+  in !i = String.length pre
 
-*)
-(* 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)