diff options
-rw-r--r-- | generic/proof-autoloads.el | 13 | ||||
-rw-r--r-- | generic/proof-config.el | 19 | ||||
-rw-r--r-- | generic/proof-menu.el | 6 | ||||
-rw-r--r-- | generic/proof-script.el | 3 |
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)) |