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 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 thread.

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 MHonArc.