Re: [isabelle] Surpress warning-squiggly lines in JEdit

On Wed, 2 Jul 2014, Moa Johansson wrote:

I would like to switch off the squiggles for warnings and stuff, it kind of makes it look like there are real errors in the theory file, when in fact there is just some message being output.

When moving from the TTY / Proof General mode to PIDE, there was indeed the effect that warnings appeared "harder" (visually more intrusive) and errors appeared "softer" (bad parts are skipped).

In the past few years I have refined this occasionally, and the process continues in the next release (you get a chance for testing within the next few days).

Stepping back from the visual and technical side-conditions there is always the semantic question where warnings are coming from (which particular tools produce them), and if there are better ways to communicate certain notable situations to the user. E.g. via messages with "bad" markup (like in 'sorry') or via "information messages" (like in the auto-check tools).


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