Add support for MMM mode

4 files changed, 37 insertions, 4 deletions

diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 4a740e51..ff9b0068 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -113,6 +113,19 @@ evaluate can be provided instead." nil 'macro)
 
 ;;;***
 
+;;;### (autoloads (proof-mmm-enable proof-mmm-support-available) "proof-mmm" "generic/proof-mmm.el")
+
+(autoload 'proof-mmm-support-available "proof-mmm" "\
+A test to see whether mmm support is available." nil nil)
+
+(autoload 'proof-mmm-enable "proof-mmm" "\
+Turn on or off MMM mode in Proof General script buffers.
+This invokes `mmm-mode' with appropriate setting for current
+buffer, and adjusts 
+on MMM regions for the prover's class." nil nil)
+
+;;;***
+
 ;;;### (autoloads nil "proof-script" "generic/proof-script.el")
 
 ;;;***
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 22f521ec..848346cd 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -114,6 +114,15 @@ whether X-Symbol is installed in your Emacs."
   :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)
+
 (defcustom proof-output-fontify-enable t
   "*Whether to fontify output from the proof assistant.
 If non-nil, output from the proof assistant will be highlighted
@@ -2058,9 +2067,13 @@ We do not force pipes everywhere because this risks loss of data."
 
 (defcustom proof-shell-strip-crs-from-input t
   "If non-nil, replace carriage returns in every input with spaces.
-This is enabled by default: it is appropriate for some systems
-because several CR's can result in several prompts, which may mess
-up the display (or even worse, the synchronization)."
+This is enabled by default: it is appropriate for many systems
+based on human input, because several CR's can result in several 
+prompts, which may mess up the display (or even worse, the 
+synchronization).  
+
+If the prover can be set to output only one prompt for every chunk of
+input, then newlines can be retained in the input."
   :type 'boolean
   :group 'proof-shell)
   
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index bac4ca71..c508e488 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -241,7 +241,7 @@ If in three window or multiple frame mode, display two buffers."
 (proof-deftoggle proof-output-fontify-enable proof-output-fontify-toggle)
 (proof-deftoggle proof-disappearing-proofs)
 (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
-
+(proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle)
 
 
 (defvar proof-quick-opts-menu
@@ -265,6 +265,10 @@ If in three window or multiple frame mode, display two buffers."
       :active (proof-x-symbol-support-maybe-available)
       :style toggle
       :selected (proof-ass x-symbol-enable)]
+     ["Multiple modes" proof-mmm-toggle
+      :active (proof-mmm-support-available)
+      :style toggle
+      :selected (proof-ass mmm-enable)]
      ["Toolbar" proof-toolbar-toggle
       ;; should really be split into :active & GNU Emacs's :visible
       :active (and (or (featurep 'toolbar) (featurep 'tool-bar))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 395a1fb7..589abe15 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2498,6 +2498,9 @@ assistant."
   
   ;; Maybe turn on x-symbol mode and MMM mode
   (proof-x-symbol-mode)
+  ;; FIXME: slight bugginess here with MMM mode/font-lock: visiting
+  ;; a fresh file leaves the progress bar up.  Perhaps turning
+  ;; on MMM here is wrong, is should happen automatically?
   (proof-mmm-enable))