Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] (Isabelle/)jEdit exception

view this post on Zulip Email Gateway (Aug 22 2022 at 11:18):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

I noticed a strange error when doing search/replace with
(Isabelle/)jEdit. The error seems to occur no matter what document is
open, even in normal text mode.

To reproduce, search/replace any non-empty string with a string that
starts or ends with a full stop (".") character. I attached the stack
trace. My hg id is e367b93f78e5; I haven't tested it with any other
Isabelle versions because I have none installed.

Cheers,

Manuel
stacktrace

view this post on Zulip Email Gateway (Aug 22 2022 at 11:41):

From: Makarius <makarius@sketis.net>
This is just a syntax error of BeanShell, trying to interpret the
replacement text as an expression.

The jEdit error dialog explains this situation further:

An error occurred while performing this operation.
Make sure the replace mode is set to "Text" if you did not intend
the replace string to be interpreted as a BeanShell expression.

Makarius

Last updated: Apr 18 2024 at 16:19 UTC