Merge PR #8843: Remove coqide ml4

11 files changed, 137 insertions, 120 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..e0ab169eda 100644
--- a/Makefile
+++ b/Makefile
@@ -78,7 +78,6 @@ LEXFILES := $(call find, '*.mll')
 YACCFILES := $(call find, '*.mly')
 export MLLIBFILES := $(call find, '*.mllib')
 export MLPACKFILES := $(call find, '*.mlpack')
-export ML4FILES := $(call find, '*.ml4')
 export MLGFILES := $(call find, '*.mlg')
 export CFILES := $(call findindir, 'kernel/byterun', '*.c')
 
@@ -94,19 +93,14 @@ EXISTINGMLI := $(call find, '*.mli')
 
 ## Files that will be generated
 
-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)
 
-# NB: all files in $(GENFILES) can be created initially, while
-# .ml files in $(GENML4FILES) might need some intermediate building.
-# That's why we keep $(GENML4FILES) out of $(GENFILES)
-
 ## More complex file lists
 
-export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML))
+export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
 
 include Makefile.common
@@ -194,7 +188,7 @@ META.coq: META.coq.in
 # Cleaning
 ###########################################################################
 
-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean
 
 clean: objclean cruftclean depclean docclean camldevfilesclean
 
@@ -202,7 +196,7 @@ cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean
 
 objclean: archclean indepclean
 
-cruftclean: ml4clean
+cruftclean: mlgclean
 	find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} +
 	rm -f gmon.out core
 
@@ -252,8 +246,8 @@ clean-ide:
 	rm -f ide/utf8_convert.ml
 	rm -rf $(COQIDEAPP)
 
-ml4clean:
-	rm -f $(GENML4FILES) $(GENMLGFILES)
+mlgclean:
+	rm -f $(GENMLGFILES)
 
 depclean:
 	find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} +
@@ -286,7 +280,7 @@ KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
 ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
 
 EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
-KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
+KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \
  $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
 KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
  $(MLIFILES:.mli=.cmi) \
@@ -308,7 +302,7 @@ include Makefile.ci
 .PHONY: tags printenv
 
 tags:
-	echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+	echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -317,12 +311,12 @@ tags:
               "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-	echo $(ML4FILES) | sort -r | xargs \
+	echo $(MLGFILES) | sort -r | xargs \
 	etags --append --language=none\
 	      "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
 
 checker-tags:
-	echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+	echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -331,7 +325,7 @@ checker-tags:
               "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-	echo $(ML4FILES) | sort -r | xargs \
+	echo $(MLGFILES) | sort -r | xargs \
 	etags --append --language=none\
 	      "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
 
diff --git a/Makefile.build b/Makefile.build
index 08863014ea..fb84a131c7 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -86,7 +86,7 @@ byte: coqbyte coqide-byte pluginsbyte printers
 
 # This list of ml files used to be in the main Makefile, we moved it here
 # to avoid exhausting the variable env in Win32
-MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
+MLFILES := $(MLSTATICFILES) $(GENMLFILES)
 
 include Makefile.common
 include Makefile.vofiles
@@ -148,7 +148,7 @@ endif
 # This include below will lauch the build of all .d.
 # The - at front is for disabling warnings about currently missing ones.
 # For creating the missing .d, make will recursively build things like
-# coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d).
+# coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d).
 
 VDFILE := .vfiles
 MLDFILE := .mlfiles
@@ -166,7 +166,7 @@ DEPENDENCIES := \
 # of include, and they will then be automatically deleted, leading to an
 # infinite loop.
 
-.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml)
+.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(MLGFILES:.mlg=.ml)
 
 ###########################################################################
 # Compilation options
@@ -259,6 +259,7 @@ CAMLP5DEPS:=grammar/grammar.cma
 CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 
 PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
+# XXX unused but should be used for mlp files
 
 # Main packages linked by Coq.
 SYSMOD:=-package num,str,unix,dynlink,threads
@@ -768,11 +769,6 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 	$(SHOW)'OCAMLYACC  $<'
 	$(HIDE)$(OCAMLYACC) --strict "$*.mly"
 
-%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP)
-	$(SHOW)'CAMLP5O   $<'
-	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \
-	  $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@
-
 %.ml: %.mlg $(COQPP)
 	$(SHOW)'COQPP   $<'
 	$(HIDE)$(COQPP) $<
@@ -782,7 +778,7 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 ###########################################################################
 
 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
-OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack
 
 MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES))
 MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES))
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/dev/tools/change-header b/dev/tools/change-header
index 61cc866602..687c02f4f1 100755
--- a/dev/tools/change-header
+++ b/dev/tools/change-header
@@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)'
 modified=0
 kept=0
 
-for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
+for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
   headline=`head -n 1 $i`
   if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then
       # Has emacs header
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)