Opened 10 years ago
Closed 9 years ago
#489 closed defect (fixed)
Electric Terminator mode breaks desktop-save-mode
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
With ProofGeneral 4.2 used for Coq (dunno about other proof assistants), desktop-save-mode breaks once I enable Electric Terminator mode. The desktop file [2] contains references to proof-electric-terminator-enable which cause errors when restarting Emacs [1], which interrupts the desktop restoring. Editing the desktop file to remove references to proof-electric-terminator-enable allows the restore to complete successfully.
The problem seems to be that proof-electric-terminator-enable takes no optional argument, while it should accept an optional argument: http://www.gnu.org/software/emacs/manual/html_node/elisp/Minor-Mode-Conventions.html
Desktop-mode does pass an optional argument to minor-mode functions to reactivate them, which fails for proof-electric-terminator-enable.
More details
The problem might boil down to the fact that desktop-save-mode passes one argument to minor mode functions - see desktop.el (on my system, it's in /Applications/Emacs?.app/Contents/Resources/lisp/desktop.el.gz):
(when (functionp minor-mode) (funcall minor-mode 1)))))))
This is with Emacs 24.3.1.
A minimal (and not really correct) workaround is to make it accept (and ignore) an argument - of course, a more correct fix would be to actually conform to the API and the convention (including naming conventions):
$ diff -u generic/pg-user.el-orig generic/pg-user.el --- generic/pg-user.el-orig 2014-03-07 17:31:33.000000000 +0100 +++ generic/pg-user.el 2014-03-07 17:31:36.000000000 +0100 @@ -506,7 +506,7 @@ proof-terminal-string))))))) ;;;###autoload -(defun proof-electric-terminator-enable () +(defun proof-electric-terminator-enable (&optional arg) "Ensure modeline update to display new value for electric terminator. This a function is called by the custom-set property 'proof-set-value." (force-mode-line-update))
This appears to work on my system.
Alternative fixes
It's true that proof-electric-terminator-toggle would accept the correct syntax, but that's not the function which gets registered (also, it only toggles the variable, but does not invoke proof-electric-terminator-enable). See this code:
(or (assq 'proof-electric-terminator-enable minor-mode-alist) (setq minor-mode-alist (append minor-mode-alist (list '(proof-electric-terminator-enable (:eval (if (eq major-mode proof-mode-for-script) proof-terminal-string)))))))
(I've tried replacing -enable with -toggle in this code, but that didn't quite work).
Moreover, this minor mode is activated for all files, not just for Coq sources - see again the excerpt from the desktop file.
To reproduce
Here are some bits necessary in .emacs to reproduce this problem:
(custom-set-variables '(proof-electric-terminator-enable t)) (desktop-save-mode 1)
After starting emacs with this configuration, load some Coq file and some non-Coq file, exit (which will save the session), and start emacs again (which should reload the session). You should get the same error.
[1] Error message:
desktop-create-buffer: Wrong number of arguments: #[nil "ÃÄ ÅÆ!)" [ad-return-value coq-double-hit-enable proof-electric-terminator-enable nil ad-Orig-proof-electric-terminator-enable coq-double-hit-toggle 0] 2 #("Advice doc string" 0 17 (ad-advice-info proof-electric-terminator-enable))], 1
[2] A relevant fragment of the desktop file:
(desktop-create-buffer 206 "/Users/pgiarrusso/.emacs" ".emacs" 'emacs-lisp-mode '(proof-electric-terminator-enable auto-complete-mode annoying-arrows-mode undo-tree-mode TeX-PDF-mode whitespace-cleanup-mode) 4508 '(1 nil) nil nil '((buffer-file-coding-system . undecided-unix))) (desktop-create-buffer 206 "/Users/pgiarrusso/Documents/Research/Sorgenti/ProofAssistants/Coq/sf/Logic.v" "Logic.v" 'coq-mode '(proof-electric-terminator-enable annoying-arrows-mode TeX-PDF-mode whitespace-cleanup-mode holes-mode) 65574 '(1 nil) nil nil '((indent-tabs-mode) (buffer-file-coding-system . undecided-unix)))
[3] From C-h m, help text showing that Proof-Electric-Terminator-Enable is indeed enabled and listed among minor modes. Proof-Active-Buffer-Fake minor mode (no indicator): Toggle active scripting mode in the current buffer. With ARG, turn on scripting iff ARG is positive.
Proof-Electric-Terminator-Enable minor mode (no indicator): Ensure modeline update to display new value for electric terminator. This a function is called by the custom-set property 'proof-set-value.
This function is advised.
After-advice `coq-unset-double-hit-advice': Disable double hit terminator since electric terminator is a replacement. This is an advice to pg `proof-electric-terminator-enable' function.
Change History (2)
comment:1 Changed 10 years ago by
comment:2 Changed 9 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Thanks for the detailed report! I have fixed proof-electric-terminator-enable to appear as a minor mode now. Please reopen if this doesn't fix your problem. - David
(Apologies for the formatting breakage above.)