Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 14:52):

From: Moa Johansson <moa.johansson@chalmers.se>
Hi,

Perhaps a stupid question, but I can’t seem to find a way to surpress the squiggly lines that JEdit puts in the proof document whenever there is some output or warning message from the command! e.g. on a function definition when it outputs that it has found a termination order and similar things.

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. But changing things under Preferences -> Plugin Options does not seem to be right...

This MUST be really simple to do this though?

Best,
Moa

Email Gateway (Aug 19 2022 at 14:53):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Moa,

although I would recommend, not to completely ignore warnings (they are
usually there for a good reasons), but you can try playing with the
colors (including transparency) to make them look more harmless.

Preferences -> Plugin Options -> Isabelle -> Rendering -> Warning Color

Dmitriy

Email Gateway (Aug 19 2022 at 15:01):

From: Carst Tankink <carst@cs.ru.nl>
On 07/02/2014 05:23 PM, Dmitriy Traytel wrote:

Hi Moa,

although I would recommend, not to completely ignore warnings (they are
usually there for a good reasons), but you can try playing with the
colors (including transparency) to make them look more harmless.

Preferences -> Plugin Options -> Isabelle -> Rendering -> Warning Color

Additionally, you might want to do the same for the "Writeln Color"
option in the same menu: this is the grey underline for output, such as
termination order. I suppose it makes more sense to 'disable' this
instead of warnings.

Carst

Dmitriy

On 02.07.2014 16:38, Moa Johansson wrote:

Hi,

Perhaps a stupid question, but I can’t seem to find a way to surpress
the squiggly lines that JEdit puts in the proof document whenever
there is some output or warning message from the command! e.g. on a
function definition when it outputs that it has found a termination
order and similar things.

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. But changing
things under Preferences -> Plugin Options does not seem to be right...

This MUST be really simple to do this though?

Best,
Moa

Email Gateway (Aug 19 2022 at 15:02):

From: Makarius <makarius@sketis.net>
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).

Makarius

Last updated: Apr 19 2024 at 20:15 UTC