Email Gateway (Aug 19 2022 at 15:55): Email Gateway (Aug 19 2022 at 15:55):From: Makarius <makarius@sketis.net>
Maybe it is just editor_reparse_limit that is too small (default 10000
characters). You could probably make this 100000.
Makarius
Email Gateway (Aug 19 2022 at 15:56):From: Gottfried Barrow <igbi@gmx.com>
Makarius,
I'll try that when I have things commented out again.
Using a batch file, I use "start Isabelle2014.exe --", and the "--"
argument works good for suppressing the loading of Scratch.thy, like you
suggested.
Concerning jEdit 5.2 changes: http://www.jedit.org/CHANGES52.txt
A welcome fix will be: "The TextArea will not scroll anymore when
dragging files on jEdit".
Regards,
GB
Email Gateway (Aug 19 2022 at 16:05):From: Gottfried Barrow <igbi@gmx.com>
Hi,
It seems like a problem like this has been covered in the past, which
might have to do with nested "(...)"s.
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.
I attach 2 screenshots. After adding an "instantiation", I had to scroll
to the bottom to clear an error. After adding the abbreviation, an error
remained at "notation", and I scrolled to the bottom to clear it.
The 1st screenshot shows the start of what's commented out, and the 2nd
shows where the commented-out section ends.
It's happening frequently, but just creating an error won't cause it to
happen. And the error is there, it "sticks" to whatever the last outer
syntax command is in the visible buffer.
Regards,
GB
140911__malformed syntax_1.png
140911__malformed syntax_2.png
Last updated: Nov 21 2024 at 12:39 UTC