Remove mmm and ML4PG contribs and remove references to them in code and docs

5 files changed, 2 insertions, 139 deletions

diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 2edf320e..0956f970 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -194,17 +194,6 @@ Currently this setting is UNIMPLEMENTED, changes have no effect."
   :set 'proof-set-value
   :group 'proof-user-options)
 
-(defpgcustom mmm-enable nil
-  "*Whether to use MMM Mode in Proof General for this assistant.
-MMM Mode allows multiple modes to be used in the same buffer.
-If you activate this variable, whether or not you really get MMM
-support depends on whether your proof assistant supports it."
-  :type 'boolean
-  :set 'proof-set-value
-  :group 'proof-user-options)
-
-
-
 (provide 'pg-custom)
 
 ;;; pg-custom.el ends here
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index ba8d1f05..67287511 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -603,26 +603,6 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
 
 ;;;***
 
-;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;;  "proof-mmm.el" (20118 50210))
-;;; Generated autoloads from proof-mmm.el
-
-(autoload 'proof-mmm-set-global "proof-mmm" "\
-Set global status of MMM mode for PG buffers to be FLAG.
-
-\(fn FLAG)" nil nil)
-
-(autoload 'proof-mmm-enable "proof-mmm" "\
-Turn on or off MMM mode in Proof General script buffer.
-This invokes `mmm-mode' to toggle the setting for the current
-buffer, and then sets PG's option for default to match.
-Also we arrange to have MMM mode turn itself on automatically
-in future if we have just activated it for this buffer.
-
-\(fn)" t nil)
-
-;;;***
-
 ;;;### (autoloads (proof-config-done proof-mode proof-insert-sendback-command
 ;;;;;;  proof-insert-pbp-command proof-script-generic-parse-find-comment-end
 ;;;;;;  proof-register-possibly-new-processed-file pg-set-span-helphighlights
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index a6f06479..aa6ddd23 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -15,28 +15,6 @@
 ;;; Code:
 
 ;;
-;; MMM
-;;
-(defun proof-mmm-support-available ()
-  "A test to see whether mmm support is available."
-  (and
-   (or (featurep 'mmm-auto)
-       (progn
-	 ;; put bundled version on load path
-	 (proof-add-to-load-path 
-		(concat proof-home-directory "contrib/mmm/"))
-	 ;; *should* always succeed unless bundled version broken
-	 (proof-try-require 'mmm-auto)))
-   ;; Load prover-specific config in <foo>-mmm.el
-   (proof-try-require (proof-ass-sym mmm))))
-
-(proof-eval-when-ready-for-assistant
-    (if (and (proof-ass mmm-enable)
-	     (proof-mmm-support-available))
-	(proof-mmm-set-global t)))
-
-
-;;
 ;; Maths menu
 ;;
 (defun proof-maths-menu-support-available ()
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index f029afcb..0a7317cb 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -329,8 +329,7 @@ without adjusting window layout."
   (proof-deftoggle-fn
    (proof-ass-sym unicode-tokens-enable) 'proof-unicode-tokens-toggle)
   (proof-deftoggle-fn
-   (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
-  (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle))
+   (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle))
 
 (defun proof-keep-response-history ()
   "Enable associated buffer histories following `proof-keep-response-history'."
@@ -381,7 +380,7 @@ without adjusting window layout."
        :style radio
        :selected (eq proof-autosend-all nil)
        :active proof-autosend-enable
-       :help "Automatically try out the next commmand"]
+       :help "Automatically try out the next command"]
        ["Send Whole Buffer"
 	(customize-set-variable 'proof-autosend-all t)
 	:style radio
@@ -525,12 +524,6 @@ without adjusting window layout."
       :selected (and (boundp 'maths-menu-mode) maths-menu-mode)
       :help "Maths menu for inserting Unicode characters"]
 
-     ["Multiple Modes" (proof-mmm-toggle (if mmm-mode 0 1))
-      :active (proof-mmm-support-available)
-      :style toggle
-      :selected (and (boundp 'mmm-mode) mmm-mode)
-      :help "Allow multiple major modes"]
-
      ["Index Menu" proof-imenu-toggle
       :active (stringp (locate-library "imenu"))
       :style toggle
@@ -578,7 +571,6 @@ without adjusting window layout."
    'proof-strict-read-only
    (proof-ass-sym unicode-tokens-enable)
    (proof-ass-sym maths-menu-enable)
-   (proof-ass-sym mmm-enable)
    'proof-toolbar-enable
    'proof-keep-response-history
    'proof-imenu-enable
diff --git a/generic/proof-mmm.el b/generic/proof-mmm.el
deleted file mode 100644
index 5d904ce3..00000000
--- a/generic/proof-mmm.el
+++ /dev/null
@@ -1,76 +0,0 @@
-;; proof-mmm.el --- Support for MMM mode package
-;;
-;; Copyright (C) 2003, 2010 LFCS Edinburgh / David Aspinall
-;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
-;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; The MMM package is at http://mmm-mode.sourceforge.net/
-;;
-;; $Id$
-;;
-;;; Commentary:
-;; 
-;; Configuration for the prover is expected to reside in <foo>-mmm.el
-;; It should define an MMM submode class called <foo>.
-;;
-;; NB: mmm-mode is bundled with Proof General, and PG will select
-;; it's own version before any other version on the Emacs load path.
-;; If you want to override this, simply load your version before
-;; starting Emacs, with (require 'mmm-auto).
-;;
-;; Credits: thanks to Stefan Monnier for pointing me to this package,
-;; and Michael Abraham Shulman for providing it.
-;;
-
-
-
-;;; Code:
-(eval-when-compile
-  (require 'cl))
-
-(eval-when-compile
-  (require 'proof-auxmodes)	  ; will be loaded
-  (require 'mmm-auto))		  ; loaded dynamically by proof-auxmodes
-
-;; The following function is called by the menu item for MMM-Mode.  It
-;; is an attempt at an intuitive behaviour without confusing the user
-;; with extra "in this buffer" and "everywhere" options.  We make the
-;; global option track the last setting made for any buffer.  The menu
-;; toggle displays the status of the buffer (as seen in the modeline)
-;; rather than the PG setting.
-
-;;;###autoload
-(defun proof-mmm-set-global (flag)
-  "Set global status of MMM mode for PG buffers to be FLAG."
-  (let ((automode-entry (list (proof-ass-sym mode) nil
-			      proof-assistant-symbol)))
-    (if flag
-	(add-to-list 'mmm-mode-ext-classes-alist
-		     automode-entry)
-      (setq mmm-mode-ext-classes-alist
-	    (delete automode-entry
-		    mmm-mode-ext-classes-alist)))
-    ;; make sure MMM obeys the mmm-mode-ext-classes-alist
-    (unless (eq mmm-global-mode t)
-      (setq mmm-global-mode 'pg-use-mode-ext-classes-alist))))
-
-;;;###autoload
-(defun proof-mmm-enable ()
-  "Turn on or off MMM mode in Proof General script buffer.
-This invokes `mmm-mode' to toggle the setting for the current
-buffer, and then sets PG's option for default to match.
-Also we arrange to have MMM mode turn itself on automatically
-in future if we have just activated it for this buffer."
-  (interactive)
-  (when (proof-mmm-support-available)
-    ;; Make sure auto mode follows PG's global setting. (NB: might do
-    ;; only if global state changes, but by now (proof-ass mmm-mode) set).
-    (with-no-warnings ; bytecomp gives spurious error
-		      ; "proof-mmm-set-global might not be defined"
-		      ; because the autoload overrides the definition above(!)
-      (proof-mmm-set-global (not mmm-mode)))
-    (mmm-mode)))
-
-(provide 'proof-mmm)
-
-;;; proof-mmm.el ends here