Custom Query (361 matches)

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.

The Proposition vernacular command is not highlighted properly.

At some point (I think related to emacs 24) Proof General changed its way for indenting lines under quantifiers. E.g.

Lemma foo_bar_baz : forall x y z,

x = y -> y = z -> x = z.

Is there a way to revert to the previous 2-space indent from the indent at the beginning of the line?