Add a configure option for disabling the compilation of why3.elc.

Moreover, this commit also performs the emacs compilation at build time
rather than install time. It also uninstalls why3.elc systematically.

Makefile.in

@@ -124,8 +124,6 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
 INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
 COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
 
-TARGET_EMACS = share/emacs/why3.elc
-
 TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
 
 ###############
@@ -290,11 +288,7 @@ clean_old_install::
 	rm -rf $(OCAMLINSTALLLIB)/why3
 
 
-ifeq ($(EMACS),no)
 install_no_local:: clean_old_install
-else
-install_no_local:: clean_old_install $(TARGET_EMACS)
-endif
 	$(MKDIR_P) $(BINDIR)
 	$(MKDIR_P) $(LIBDIR)/why3
 	$(MKDIR_P) $(TOOLDIR)
@@ -305,7 +299,6 @@ endif
 	$(MKDIR_P) $(DATADIR)/why3/theories
 	$(MKDIR_P) $(DATADIR)/why3/modules/mach
 	$(MKDIR_P) $(DATADIR)/why3/drivers
-	$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
 	$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
 	$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
 	$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
@@ -355,16 +348,19 @@ uninstall: clean_old_install
 
 clean_old_install::
 	rm -f $(DATADIR)/emacs/site-lisp/why3.el
-ifneq ($(EMACS),no)
 	rm -f $(DATADIR)/emacs/site-lisp/why3.elc
-endif
 
 install_no_local::
+	$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
 	$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
-ifneq ($(EMACS),no)
+ifeq (@enable_emacs_compilation@,yes)
 	$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
 endif
 
+ifeq (@enable_emacs_compilation@,yes)
+opt byte: share/emacs/why3.elc
+endif
+
 
 ##################
 # Why3 plugins

configure.in

@@ -127,6 +127,12 @@ AC_ARG_ENABLE(profiling,
     AS_HELP_STRING([--enable-profiling], [enable profiling]),,
     enable_profiling=no)
 
+# Emacs compilation
+
+AC_ARG_ENABLE(emacs-compilation,
+    AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
+    enable_emacs_compilation=yes)
+
 # either relocation or local, not both
 if test "$enable_relocation" = yes ; then
 if test "$enable_local" = yes ; then
@@ -351,7 +357,13 @@ if test "$enable_html_doc" = yes ; then
 fi
 
 # checking for emacs
-AC_CHECK_PROG(EMACS,emacs,emacs,no)
+if test "$enable_emacs_compilation" = yes ; then
+   AC_CHECK_PROG(EMACS,emacs,emacs,no)
+   if test "$EMACS" = no ; then
+      enable_emacs_compilation=no
+      AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
+   fi
+fi
 
 # checking for Zarith
 if test "$enable_zarith" = yes; then
@@ -790,6 +802,8 @@ AC_SUBST(enable_html_doc)
 AC_SUBST(RUBBER)
 AC_SUBST(HEVEA)
 AC_SUBST(HACHA)
+
+AC_SUBST(enable_emacs_compilation)
 AC_SUBST(EMACS)
 
 AC_SUBST(enable_frama_c)