Select OS specific coqide code with cp.

9 files changed, 121 insertions, 94 deletions

diff --git a/.gitignore b/.gitignore
index 709e87cc9c..f9e43a0eb7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -139,7 +139,7 @@ plugins/ltac/coretactics.ml
 plugins/ltac/extratactics.ml
 plugins/ltac/extraargs.ml
 plugins/ltac/profile_ltac_tactics.ml
-ide/coqide_main.ml
+ide/coqide_os_specific.ml
 plugins/ssrmatching/ssrmatching.ml
 plugins/ssr/ssrparser.ml
 plugins/ssr/ssrvernac.ml
diff --git a/Makefile b/Makefile
index f2dc6d7750..b9d8bf34e3 100644
--- a/Makefile
+++ b/Makefile
@@ -96,7 +96,7 @@ EXISTINGMLI := $(call find, '*.mli')
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
diff --git a/Makefile.ide b/Makefile.ide
index 6c069a1e50..39af1f8545 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -49,8 +49,8 @@ IDETOPEXE=bin/coqidetop$(EXE)
 IDETOP=bin/coqidetop.opt$(EXE)
 IDETOPBYTE=bin/coqidetop.byte$(EXE)
 
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml
 
 IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
 
@@ -110,10 +110,10 @@ $(COQIDEBYTE): $(LINKIDE)
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
 	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
-ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here
-	$(SHOW)'CAMLP5O   $<'
-	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@
-
+ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
+	@rm -f $@
+	cp $< $@
+	@chmod -w $@
 
 ide/%.cmi: ide/%.mli
 	$(SHOW)'OCAMLC    $<'
diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in
new file mode 100644
index 0000000000..a08bac5772
--- /dev/null
+++ b/ide/coqide_QUARTZ.ml.in
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let osx = GosxApplication.osxapplication ()
+
+let () =
+  let _ = osx#connect#ns_application_open_file
+    ~callback:(fun x -> Coqide.do_load x; true)
+  in
+  let _ = osx#connect#ns_application_block_termination
+    ~callback:Coqide.forbid_quit
+  in
+  let _ = osx#connect#ns_application_will_terminate
+    ~callback:Coqide.close_and_quit
+  in ()
+
+let init () =
+  let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication
+    (GtkMenu.MenuShell.cast
+       (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget)
+  in
+  let () = GtkosxApplication.Application.insert_app_menu_item
+    osx#as_osxapplication
+    (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1
+  in
+  let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication
+    (Some (GtkMenu.MenuItem.cast
+             (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget))
+  in
+  osx#ready ()
diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in
new file mode 100644
index 0000000000..8c4649fc39
--- /dev/null
+++ b/ide/coqide_WIN32.ml.in
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* On win32, we add the directory of coqide to the PATH at launch-time
+   (this used to be done in a .bat script). *)
+
+let set_win32_path () =
+  Unix.putenv "PATH"
+    (Filename.dirname Sys.executable_name ^ ";" ^
+      (try Sys.getenv "PATH" with _ -> ""))
+
+(* On win32, since coqide is now console-free, we re-route stdout/stderr
+   to avoid Sys_error if someone writes to them. We write to a pipe which
+   is never read (by default) or to a temp log file (when in debug mode).
+*)
+
+let reroute_stdout_stderr () =
+  (* We anticipate a bit the argument parsing and look for -debug *)
+  let debug = List.mem "-debug" (Array.to_list Sys.argv) in
+  Minilib.debug := debug;
+  let out_descr =
+    if debug then
+      let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
+      Coqide.logfile := Some name;
+      Unix.descr_of_out_channel chan
+    else
+      snd (Unix.pipe ())
+  in
+  Unix.set_close_on_exec out_descr;
+  Unix.dup2 out_descr Unix.stdout;
+  Unix.dup2 out_descr Unix.stderr
+
+(* We also provide specific kill and interrupt functions. *)
+
+external win32_kill : int -> unit = "win32_kill"
+external win32_interrupt : int -> unit = "win32_interrupt"
+let () =
+  Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
+  set_win32_path ();
+  Coq.interrupter := win32_interrupt;
+  reroute_stdout_stderr ()
+
+let init () = ()
diff --git a/ide/coqide_X11.ml.in b/ide/coqide_X11.ml.in
new file mode 100644
index 0000000000..6a5784eac3
--- /dev/null
+++ b/ide/coqide_X11.ml.in
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let init () = ()
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml
index 3a92e1bc91..91e8be875a 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml
@@ -49,88 +49,6 @@ let catch_gtk_messages () =
 
 let () = catch_gtk_messages ()
 
-
-
-(** System-dependent settings *)
-
-let os_specific_init () = ()
-
-(** Win32 *)
-
-IFDEF WIN32 THEN
-
-(* On win32, we add the directory of coqide to the PATH at launch-time
-   (this used to be done in a .bat script). *)
-
-let set_win32_path () =
-  Unix.putenv "PATH"
-    (Filename.dirname Sys.executable_name ^ ";" ^
-      (try Sys.getenv "PATH" with _ -> ""))
-
-(* On win32, since coqide is now console-free, we re-route stdout/stderr
-   to avoid Sys_error if someone writes to them. We write to a pipe which
-   is never read (by default) or to a temp log file (when in debug mode).
-*)
-
-let reroute_stdout_stderr () =
-  (* We anticipate a bit the argument parsing and look for -debug *)
-  let debug = List.mem "-debug" (Array.to_list Sys.argv) in
-  Minilib.debug := debug;
-  let out_descr =
-    if debug then
-      let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
-      Coqide.logfile := Some name;
-      Unix.descr_of_out_channel chan
-    else
-      snd (Unix.pipe ())
-  in
-  Unix.set_close_on_exec out_descr;
-  Unix.dup2 out_descr Unix.stdout;
-  Unix.dup2 out_descr Unix.stderr
-
-(* We also provide specific kill and interrupt functions. *)
-
-external win32_kill : int -> unit = "win32_kill"
-external win32_interrupt : int -> unit = "win32_interrupt"
-let () =
-  Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
-  set_win32_path ();
-  Coq.interrupter := win32_interrupt;
-  reroute_stdout_stderr ()
-END
-
-(** MacOSX *)
-
-IFDEF QUARTZ THEN
-let osx = GosxApplication.osxapplication ()
-
-let () =
-  let _ = osx#connect#ns_application_open_file
-    ~callback:(fun x -> Coqide.do_load x; true)
-  in
-  let _ = osx#connect#ns_application_block_termination
-    ~callback:Coqide.forbid_quit
-  in
-  let _ = osx#connect#ns_application_will_terminate
-    ~callback:Coqide.close_and_quit
-  in ()
-
-let os_specific_init () =
-  let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication
-    (GtkMenu.MenuShell.cast
-       (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget)
-  in
-  let () = GtkosxApplication.Application.insert_app_menu_item
-    osx#as_osxapplication
-    (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1
-  in
-  let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication
-    (Some (GtkMenu.MenuItem.cast
-             (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget))
-  in
-  osx#ready ()
-END
-
 let load_prefs () =
   try Preferences.load_pref ()
   with e -> Ideutils.flash_info
@@ -145,7 +63,7 @@ let () =
   Coq.check_connection args;
   Coqide.sup_args := args;
   Coqide.main files;
-  os_specific_init ();
+  Coqide_os_specific.init ();
   try
     GMain.main ();
     failwith "Gtk loop ended"
diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli
new file mode 100644
index 0000000000..ebd09099f0
--- /dev/null
+++ b/ide/coqide_os_specific.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val init : unit -> unit
diff --git a/ide/dune b/ide/dune
index 70a1709f37..5714b1370e 100644
--- a/ide/dune
+++ b/ide/dune
@@ -33,9 +33,9 @@
  (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
 
 (rule
- (targets coqide_main.ml)
- (deps (:ml4-file coqide_main.ml4))
- (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets})))
+ (targets coqide_os_specific.ml)
+ (deps (:in-file coqide_X11.ml.in)) ; TODO support others
+ (action (run cp %{in-file} %{targets})))
 
 (executable
  (name coqide_main)