Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange behaviour with CVS Proof General and e...

view this post on Zulip Email Gateway (Aug 18 2022 at 12:21):

From: Stephan Hohe <sth.lists@tejp.de>
Clemens Ballarin wrote:
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

view this post on Zulip Email Gateway (Aug 18 2022 at 12:25):

From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hi,

Does anyone else experience an emacs freeze after typing @{ in a
text {* *} block? Typing {} and putting the @ in later works fine.
I don't have any idea where it's happening, so I can't file a decent PG
bug report...

I'm using the latest PG from CVS and
GNU Emacs 23.0.60.1 (x86_64-pc-linux-gnu, GTK+ Version 2.12.9)
of 2008-05-07 on osmium, modified by Debian

I'm not sure if this is the right list to post this, but I'm sure if
someone's experienced this, they're here.

Sincerely,

Rafal Kolanski.

view this post on Zulip Email Gateway (Aug 18 2022 at 12:26):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Rafal,

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

I then went back to 3.7.1pre080722, which behaves a bit better.

Clemens

Last updated: May 03 2024 at 01:09 UTC