Re: [isabelle] Malformed syntax error clears only on scroll to bottom
On Thu, 11 Sep 2014, Gottfried Barrow wrote:
I get "malformed command syntax" errors after sometimes adding source
above some source I have commented out almost to the "end" of the
document. Normally errors clear when I finally satisfy all the syntax
requirements, but for these, I have to scroll to the bottom of the
document to get them to clear.
Maybe it is just editor_reparse_limit that is too small (default 10000
characters). You could probably make this 100000.
This archive was generated by a fusion of
Pipermail (Mailman edition) and