Re: [isabelle] Message output in Isabelle2014 and Isabelle2015

On 23/06/2015 18:52, Makarius wrote:
On Tue, 23 Jun 2015, Tobias Nipkow wrote:

I recommend to reread Gerwin's comment on red squiggles in the earlier thread:

Iâm not as worried about the scrolling as Peter (you could set goals_limit for
instance, although Iâd prefer not to have to), but I do have to point out that
the squiggles canât be the main interaction mechanism for errors. They are
popups: you have to pick up the mouse, navigate there, and wait to see them.
If the statement is big, the message sometimes obscures what you typed. That's
too disruptive as main mechanism.

Itâs good to have the squiggles for errors (esp for position indication), and
they work very well for warnings, but when youâre writing your proof, your
brain doesnât work as asynchronously as the document model. You will still
have your mental focus at one point and you will still want to see the result
of your last action as quickly as possible and react if it is an error. When
youâre writing the proof, your mental focus is on the output window, so thatâs
where errors reports will cause the least mental overhead.

I read that, and it is one of the few things that are not rubbish on the other

Speak for yourself, but don't insult other contributors to this list. We don't call red squiggols rubbish either.


Gerwin merely described observations, without pretending to know how things work
or how they should be done.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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