Re: [isabelle] Message output in Isabelle2014 and Isabelle2015
On Tue, 23 Jun 2015, Tobias Nipkow wrote:
I recommend to reread Gerwin's comment on red squiggles in the earlier
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
Gerwin merely described observations, without pretending to know how
things work or how they should be done.
This archive was generated by a fusion of
Pipermail (Mailman edition) and