Opened 13 years ago

Closed 13 years ago

#236 closed defect (fixed)

Crash when entering antiquotation

Reported by: Clemens Ballarin Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords:


Entering @{ is broken in 3.7.1 and later. Effect: emacs takes three minutes to respond if it doesn't crash!!! It works with 3.7.1pre080722.

This is on GNU Emacs 22.2.1 (i386-apple-darwin8.11.1, Carbon Version 1.6.0) of 2008-04-02 on seijiz.local.

Change History (5)

comment:1 Changed 13 years ago by Clemens Ballarin

Actually, in 3.7.1pre080722 processing @{ and what comes before the closing } can still be slow. It seems fine if you type slowly but it tends to block for a few seconds if you type fast.

comment:2 Changed 13 years ago by David Aspinall

Status: newaccepted

Yuk! What a nasty problem. I notice that it also seems to depend on how much you write in an antiquotation. As a workaround, simply type the closing brace } and then fill in between.

This seems to be caused by bad behaviour in regexp matching (C code, hence hard crash) caused by the font lock pattern for antiquotations. We have seen this before, see the comment in code in isar-syntax.el:

;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
;; incomplete antiquotations like @{text bla"} (even though it is supposed to
;; stop at eol anyway).

(defconst isar-antiq-regexp
  (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
  "Regexp matching Isabelle/Isar antiquoations.")

A change since the previous versions is the position of this pattern in the font-lock regexps (token highlighting is handled by Unicode Tokens mode now), but the pattern itself is unchanged. Earlier in the history we had some other workarounds that might be reinstated.

Further investigations to suggest a simpler expression matching, or an isolated test case to send to the GNU Emacs maintainers, would be very useful.

comment:3 Changed 13 years ago by David Aspinall

Removing the shy matching ?: doesn't help.

comment:4 Changed 13 years ago by Clemens Ballarin

Stephan Hohe posted the following suggestions of a fix/workaround to isabelle-users:

The problem is probably the following regex in the ProofGeneral syntax file (ProofGeneral/isar/isar-syntax.el):

| (defconst isar-antiq-regexp | (concat "@{
|" isar-string "
}}") | "Regexp matching Isabelle/Isar? antiquoations.")

It matches either several characters, or an isar-string, multiple times, searching for a closing "}". If there are no isar-strings this basically comes down to "\([\"{}]+\)+}", and this matches "several groups of several characters, followed by }". Emacs seems to try all possible combinations in search for the closing "}".

I would suggest:

| (defconst isar-antiq-regexp | (concat "@{
|" isar-string "
)*}") | "Regexp matching Isabelle/Isar? antiquoations.")

This avoids the nested "+" and even works for anti-quotations with more then ten isar-strings.

I would add this comment to the ProofGeneral bug, but registration of new users seems to be broken there.

comment:5 Changed 13 years ago by David Aspinall

Resolution: fixed
Status: acceptedclosed

Thanks for posts/emails. Stephan's fix is now in CVS.

Note: See TracTickets for help on using tickets.