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

9 files changed, 147 insertions, 52 deletions

diff --git a/Makefile.build b/Makefile.build
index feb09fd57..2f5b43303 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -309,12 +309,14 @@ coqide-files: $(IDEFILES)
 
 $(COQIDEOPT): $(LINKIDEOPT) $(LIBCOQRUN) $(COQTOPOPT)
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa gtkThread.cmx dynlink.cmxa str.cmxa $(CAMLP4MOD).cmxa $(LIBCOQRUN) $(LINKIDEOPT)
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\
+		 gtkThread.cmx dynlink.cmxa str.cmxa $(CAMLP4MOD).cmxa $(LIBCOQRUN) $(LINKIDEOPT)
 	$(STRIP) $@
 
 $(COQIDEBYTE): $(LINKIDE) $(LIBCOQRUN) $(COQTOPBYTE)
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo dynlink.cma str.cma $(CAMLP4MOD).cma $(COQRUNBYTEFLAGS) $(LIBCOQRUN) $(LINKIDE)
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\
+		dynlink.cma str.cma $(CAMLP4MOD).cma $(COQRUNBYTEFLAGS) $(LIBCOQRUN) $(LINKIDE)
 
 $(COQIDE):
 	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
@@ -694,6 +696,15 @@ toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@
 
+ide/coqide_main.ml: ide/coqide_main.ml4
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4USE) -impl $< -o $@
+
+ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4USE) $(IDEOPTP4) -impl $< -o $@
+
+
 # pretty printing of the revision number when compiling a checked out
 # source tree
 .PHONY: revision
diff --git a/Makefile.common b/Makefile.common
index 9e45758c4..b2581776a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -220,7 +220,7 @@ LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 IDECMA:=ide/ide.cma
 
 LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTDEPS) $(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml
 
 # modules known by the toplevel of Coq
 
diff --git a/config/Makefile.template b/config/Makefile.template
index 8000c6169..cd92fc446 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -138,6 +138,9 @@ STRIP=STRIPCOMMAND
 
 # CoqIde (no/byte/opt)
 HASCOQIDE=COQIDEOPT
+IDEOPTFLAGS=MACIGEFLAGS
+IDEOPTDEPS=MACIGEFILE
+IDEOPTP4=MACIGEP4
 
 # Defining REVISION
 CHECKEDOUT=CHECKEDOUTSOURCETREE
diff --git a/configure b/configure
index c30c71414..360e28685 100755
--- a/configure
+++ b/configure
@@ -71,6 +71,8 @@ usage () {
     printf "\tSpecifies whether or not to use dynamic loading of native code\n"
     echo "-coqide (opt|byte|no)"
     printf "\tSpecifies whether or not to compile Coqide\n"
+    echo "-nomacintegration"
+    printf "\tSpecifies to not try to build coqide mac integration\n"
     echo "-browser <command>"
     printf "\tUse <command> to open URL %%s\n"
     echo "-with-doc (yes|no)"
@@ -136,6 +138,7 @@ lablgtkdir_spec=no
 coqdocdir_spec=no
 arch_spec=no
 coqide_spec=no
+nomacintegration_spec=no
 browser_spec=no
 wwwcoq_spec=no
 with_geoproof=false
@@ -221,6 +224,8 @@ while : ; do
 			  *) COQIDE=no
 		      esac
 		      shift;;
+    -nomacintegration) nomacintegration_spec=yes
+		      shift;;
     -browser|--browser) browser_spec=yes
 		      BROWSER=$2
 		      shift;;
@@ -289,16 +294,16 @@ case $arch_spec in
 	ARCH="win32"
     else
 	# If not, we determine the architecture
-	if test -x /bin/arch ; then
+	if test -x /bin/uname ; then
+ 	    ARCH=`/bin/uname -s`
+ 	elif test -x /usr/bin/uname ; then
+ 	    ARCH=`/usr/bin/uname -s`
+ 	elif test -x /bin/arch ; then
  	    ARCH=`/bin/arch`
  	elif test -x /usr/bin/arch ; then
  	    ARCH=`/usr/bin/arch`
  	elif test -x /usr/ucb/arch ; then
  	    ARCH=`/usr/ucb/arch`
- 	elif test -x /bin/uname ; then
- 	    ARCH=`/bin/uname -s`
- 	elif test -x /usr/bin/uname ; then
- 	    ARCH=`/usr/bin/uname -s`
 	else
 	    echo "I can not automatically find the name of your architecture."
 	    printf "%s"\
@@ -370,6 +375,7 @@ fi
 if [ "$browser_spec" = "no" ]; then
     case $ARCH in
         win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
+	Darwin) BROWSER='open %s' ;;
         *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
     esac
 fi
@@ -471,7 +477,7 @@ else
     HASNATDYNLINK=false
 fi
 
-case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in
+case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in
     true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
         NATDYNLINKFLAG=os5fixme;;
     #Possibly a problem on 10.6.0/10.6.1/10.6.2
@@ -634,9 +640,20 @@ else
     elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then 
 	echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
 	COQIDE=byte
-    else 
-	echo "LablGtk2 found, native threads: native CoqIde will be available."
+    else
+        echo "LablGtk2 found, native threads: native CoqIde will be available."
 	COQIDE=opt
+        if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
+            then 
+            cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
+            MACIGEFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
+            MACIGEFILE=ide/macjokes.o
+            MACIGEP4=-DMacInt
+            else
+            MACIGEFLAGS=""
+            MACIGEFILE=""
+            MACIGEP4=""
+            fi
     fi
 fi
 
@@ -657,9 +674,14 @@ case $ARCH in
     win32)
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
+    Darwin) if [ "$HASNATDYNLINK" = "true" ]
+	then
+	  STRIPCOMMAND="true"
+	else
+	  STRIPCOMMAND="strip"
+	fi;;
     *)
-    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
-       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]
     then
 	STRIPCOMMAND="true"
     else
@@ -805,7 +827,7 @@ esac
 
 # Determine if we enable -custom by default (Windows and MacOS)
 CUSTOM_OS=no
-if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
+if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then
     CUSTOM_OS=yes
 fi
 
@@ -859,6 +881,9 @@ fi
 if test "$COQIDE" != "no"; then
 echo "  Lablgtk2 library in               : $LABLGTKLIB"
 fi
+if test "$MACIGEFILE" != ""; then
+echo "  Mac OS integration is on"
+fi
 if test "$with_doc" = "all"; then
 echo "  Documentation                     : All"
 else
@@ -1088,6 +1113,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|RANLIBEXEC|$ranlib_exec|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
     -e "s|COQIDEOPT|$COQIDE|" \
+    -e "s|MACIGEFLAGS|$MACIGEFLAGS|" \
+    -e "s|MACIGEFILE|$MACIGEFILE|" \
+    -e "s|MACIGEP4|$MACIGEP4|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
     -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
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);
+}