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