[isabelle] Malformed syntax error clears only on scroll to bottom



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

Attachment: 140911__malformed syntax_1.png
Description: PNG image

Attachment: 140911__malformed syntax_2.png
Description: PNG image



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