Custom Query (361 matches)

Hello! I use Proof General with Coq, Utoks mode is enabled.

When I enter a string:

Case "".<newline>

Emacs stops responding. It's really annoying, since it's used in the course I'm trying to go through: ​http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28

I can reproduce a bug on my PC:

1. visit a new (or old) file with .v extension
2. type:

Case "".

3. Press "enter" button on keyboard (that is, to make new line)

Please help me with that!

I'm neither an Emacs nor Proof-General pro, so I'm not sure what should I do and what should I tell you.

I have some relevant to PG settings in my .emacs.d/init.el file:

(require 'unicode-tokens)

(add-hook 'coq-mode-hook
          (lambda ()
            (proof-unicode-tokens-enable)
            ))

(add-hook 'unicode-tokens-mode-hook
          (lambda ()
            (unicode-tokens-show-symbols)
            (local-set-key (kbd "s-v") 'unicode-tokens-paste)))

I use PG 4.1RC2. Emacs: GNU Emacs 24.0.50.1 (i386-apple-darwin10.7.3, NS apple-appkit-1038.35) on Mac OS X Lion.

Using GNU emacs 22.1.1 on Ubuntu 7.10, the editor occasionally hangs when doing isearch-forward.

E.g. reproduce this by visiting Isabelle/src/HOL/Lambda/WeakNorm.thy: type C-s, type "c" "o" "n" "s" (which finds an occurreny of "Cons" in the text), continuing to type "t" makes emacs hang; after C-g it works again, but there is some danger it will again hang later.

The devlopment version (BZR trunk) of Emacs can hang when PG Coq is used together with Emacs' auto fill minor mode. You can, for instance, reproduce the error in the following way:

1. Start Emacs without any initialization; emacs -q -nsl
2. Load PG initialization: M-x load-file <path-to-PG>/generic/proof-site.el
3. Open a *.v file.
4. Activate auto fill mode: M-x auto-fill-mode
5. Place the cursor _afer_ a comment with more than `fill-column' many characters.
6. Press <enter> -> Emacs hangs, and must be killed.

Remark 1: You do not get an error if auto filling happens _inside_ a comment.

Remark 2: Emacs 24.2.1 does not have this problem at all.