[isabelle-dev] Code Folding and errors

[Peter Lammich]

Feature Request: (Isabelle: caae34eabcef)

If an error appears in folded code, make it somehow visible in the main
text window. 

Currently, there is no indication of such an error that allows precise
localization. Trying to jump to the error via clicking on the red bars
on the left requires very precise clicking to actually unfold the
content with the error: If the theory is large, it may even be
impossible. 

This is particular annoying when changing existing theories: One wants
to use folding to get a better overview of the theory, and, at the same
time, must be able to quickly locate errors introduced by one's
changes.


Proposal: Display the red exclamation mark icon on the folded line, if
there is an error in the folded content.

--
  Peter