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:
> 
>   http://proofgeneral.inf.ed.ac.uk/trac/ticket/236

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.

/Stephan





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