Re: [isabelle] Strange behaviour with CVS Proof General and emacs

Clemens Ballarin wrote:
>> Does anyone else experience an emacs freeze after typing @{ in a
>> text {*  *} block? Typing {} and putting the @ in later works fine.
> Yes!  And I've already filed a bug report a while ago:

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

| (defconst isar-antiq-regexp
|   (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
|   "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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.