Re: [isabelle] (Isabelle/)jEdit exception
On Tue, 22 Sep 2015, Manuel Eberl wrote:
To reproduce, search/replace any non-empty string with a string that
starts or ends with a full stop (".") character. I attached the stack
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and