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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev