MacOS integration

if `pkg-config --exists ige-mac-integration`, coqide.opt will be
able to open files by double-clik in finder on Darwin.

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

5 files changed, 91 insertions, 38 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 708835b93..5ebea7589 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3162,38 +3162,3 @@ let process_argv argv =
     filtered
   with _ ->
     (output_string stderr "coqtop choked on one of your option"; exit 1)
-
-let start () =
-  let argl = Array.to_list Sys.argv in
-  let files = process_argv argl in
-  let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
-  sup_args := String.concat " " (List.map Filename.quote args);
-  check_connection !sup_args;
-  ignore_break ();
-    GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
-    (try
-	 GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
-     with Not_found -> ());
-    ignore (GtkMain.Main.init ());
-    GtkData.AccelGroup.set_default_mod_mask
-      (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
-    ignore (
-	     Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
-								 `WARNING;`CRITICAL]
-	       (fun ~level msg ->
-		  if level land Glib.Message.log_level `WARNING <> 0
-		  then Pp.warning msg
-		  else failwith ("Coqide internal error: " ^ msg)));
-    main files;
-    if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
-    while true do
-      try
-	GtkThread.main ()
-      with
-	| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
-	| e ->
-	    Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
-	    flush stderr;
-	    crash_save 127
-    done
-
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 3522bee44..cac6878cd 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -10,5 +10,10 @@
    command line, initialize the load path, load the input
    state, load the files given on the command line, load the ressource file,
    produce the output state if any, and finally will launch the interface. *)
-
-val start : unit -> unit
+val sup_args : string ref
+val do_load : string -> unit
+val process_argv : string list -> string list
+val crash_save : int -> unit
+val ignore_break : unit -> unit
+val check_for_geoproof_input : unit -> unit
+val main : string list -> unit
diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
deleted file mode 100644
index 52c956c3c..000000000
--- a/ide/coqide_main.ml
+++ /dev/null
@@ -1 +0,0 @@
-let () = Coqide.start ()
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
new file mode 100644
index 000000000..6e36df6d1
--- /dev/null
+++ b/ide/coqide_main.ml4
@@ -0,0 +1,47 @@
+IFDEF MacInt THEN
+external gtk_mac_init : (string -> unit) -> unit
+  = "caml_gtk_mac_init"
+
+external gtk_mac_ready : unit -> unit
+  = "caml_gtk_mac_ready"
+END
+
+let initmac () = IFDEF MacInt THEN gtk_mac_init Coqide.do_load ELSE () END
+
+let macready () = IFDEF MacInt THEN gtk_mac_ready () ELSE ()  END
+
+let () =
+  let argl = Array.to_list Sys.argv in
+  let files = Coqide.process_argv argl in
+  let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
+  Coqide.sup_args := String.concat " " (List.map Filename.quote args);
+  Coq.check_connection !Coqide.sup_args;
+  Coqide.ignore_break ();
+    GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc");
+    (try
+	 GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
+     with Not_found -> ());
+    ignore (GtkMain.Main.init ());
+    initmac () ;
+(*    GtkData.AccelGroup.set_default_mod_mask
+      (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*)
+    ignore (
+	     Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
+								 `WARNING;`CRITICAL]
+	       (fun ~level msg ->
+		  if level land Glib.Message.log_level `WARNING <> 0
+		  then Pp.warning msg
+		  else failwith ("Coqide internal error: " ^ msg)));
+    Coqide.main files;
+    if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
+    macready () ;
+    while true do
+      try
+	GtkThread.main ()
+      with
+	| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
+	| e ->
+	    Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
+	    flush stderr;
+	    Coqide.crash_save 127
+    done
diff --git a/ide/macjokes.c b/ide/macjokes.c
new file mode 100644
index 000000000..84d222ae9
--- /dev/null
+++ b/ide/macjokes.c
@@ -0,0 +1,37 @@
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+#include <caml/callback.h>
+#include <caml/fail.h>
+
+#include <igemacintegration/gtkosxapplication.h>
+
+GtkOSXApplication *theApp;
+value open_file_fun;
+
+static gboolean deal_with_open(GtkOSXApplication *app, gchar *path, gpointer user_data)
+{
+  CAMLparam0();
+  CAMLlocal2(string_path, res);
+  string_path = caml_copy_string(path);
+  res = caml_callback_exn(open_file_fun,string_path);
+  gboolean truc = !(Is_exception_result(res));
+  CAMLreturnT(gboolean, truc);
+}
+
+CAMLprim value caml_gtk_mac_init(value open_file_the_fun)
+{
+  CAMLparam1(open_file_the_fun);
+  open_file_fun = open_file_the_fun;
+  caml_register_generational_global_root(&open_file_fun);
+  theApp = g_object_new(GTK_TYPE_OSX_APPLICATION, NULL);
+  g_signal_connect(theApp, "NSApplicationOpenFile", G_CALLBACK(deal_with_open), NULL);
+  CAMLreturn (Val_unit);
+}
+
+CAMLprim value caml_gtk_mac_ready(value unit)
+{
+  CAMLparam1(unit);
+  gtk_osxapplication_ready(theApp);
+  CAMLreturn(Val_unit);
+}