From c9e9c691c353d5d4835551de8d7d1f4c0ec74b9f Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 24 May 2017 11:14:51 -0400 Subject: Remove mmm and ML4PG contribs and remove references to them in code and docs --- generic/pg-custom.el | 11 ------- generic/proof-autoloads.el | 20 ------------ generic/proof-auxmodes.el | 22 -------------- generic/proof-menu.el | 12 ++------ generic/proof-mmm.el | 76 ---------------------------------------------- 5 files changed, 2 insertions(+), 139 deletions(-) delete mode 100644 generic/proof-mmm.el (limited to 'generic') 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 @@ -601,26 +601,6 @@ Construct and return PG auxiliary menu used in non-scripting buffers. \(fn)" nil nil) -;;;*** - -;;;### (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 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 @@ -14,28 +14,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 -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 ;; 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 -;; 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 -mmm.el -;; It should define an MMM submode class called . -;; -;; 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 -- cgit v1.2.3