Ide: Drop argument added by MacOS during .app launch

5 files changed, 23 insertions, 10 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9614c6f3b..a9bc60d14 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -568,11 +568,11 @@ let get_current_word term =
 
 let print_branch c l =
   Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
-    (print_list (fun c s -> Format.fprintf c "%s@ " s)) l
+    (Minilib.print_list (fun c s -> Format.fprintf c "%s@ " s)) l
 
 let print_branches c cases =
   Format.fprintf c "@[match var with@\n%aend@]@."
-    (print_list print_branch) cases
+    (Minilib.print_list print_branch) cases
 
 let display_match sn = function
   |Interface.Fail _ ->
@@ -1387,6 +1387,9 @@ let read_coqide_args argv =
     |"-coqtop-flags" :: flags :: args->
       Flags.ideslave_coqtop_flags := Some flags;
       filter_coqtop coqtop project_files out args
+    |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg ->
+      (* argument added by MacOS during .app launch *)
+      filter_coqtop coqtop project_files out args
     |arg::args -> filter_coqtop coqtop project_files (arg::out) args
     |[] -> (coqtop,List.rev project_files,List.rev out)
   in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 424c41a60..945e425c6 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -253,11 +253,6 @@ let coqtop_path () =
 	  with Not_found -> "coqtop"
   in file
 
-let rec print_list print fmt = function
-  | [] -> ()
-  | [x] -> print fmt x
-  | x :: r -> print fmt x; print_list print fmt r
-
 (* 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/ideutils.mli b/ide/ideutils.mli
index 5877d1270..657e92869 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -40,9 +40,6 @@ val stock_to_widget :
   ?size:[`CUSTOM of int * int | Gtk.Tags.icon_size] ->
     GtkStock.id -> GObj.widget
 
-open Format
-val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
-
 val custom_coqtop : string option ref
 (* @return command to call coqtop
    - custom_coqtop if set
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 6a960e266..d11e8c56b 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -6,6 +6,11 @@
 (*         *       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
@@ -53,3 +58,13 @@ 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
+
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 0508dbf83..b7672c900 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -9,6 +9,8 @@
 (** Some excerpts of Util and similar files to avoid depending on them
     and hence on Compat and Camlp4 *)
 
+val print_list : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+
 type level = [
   | `DEBUG
   | `INFO
@@ -25,3 +27,4 @@ val log : ?level:level -> string -> unit
 val coqide_config_home : unit -> string
 val coqide_config_dirs : unit -> string list
 val coqide_data_dirs : unit -> string list
+val is_prefix_of : string -> string -> bool