Custom Query (361 matches)


Show under each result:

Results (13 - 15 of 361)

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Ticket Resolution Summary Owner Reporter
#489 fixed Electric Terminator mode breaks desktop-save-mode David Aspinall coquser

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:

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 @@

-(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."

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
			   (if (eq major-mode proof-mode-for-script)

(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:

 '(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
  '(proof-electric-terminator-enable auto-complete-mode annoying-arrows-mode undo-tree-mode TeX-PDF-mode whitespace-cleanup-mode)
  '(1 nil)
  '((buffer-file-coding-system . undecided-unix)))

(desktop-create-buffer 206
  '(proof-electric-terminator-enable annoying-arrows-mode TeX-PDF-mode whitespace-cleanup-mode holes-mode)
  '(1 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.

#487 fixed Coq syntax highlighting: Proposition David Aspinall coquser

The Proposition vernacular command is not highlighted properly.

#486 fixed Disable long indention under quantifiers? courtieu coquser

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?

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Note: See TracQuery for help on using queries.