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.


	Makarius




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