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 trace.

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




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