Re: [isabelle] Message output in Isabelle2014 and Isabelle2015




On 23/06/2015 16:51, Makarius wrote:
The current printing of goal state errors is the result of various reforms in
the past few years. That relatively new behaviour is actually the reason why I
usually do many things without ever looking at the Output window, often having
it closed over a long stretch of time: the message under the red squiggles
usually provides the relevant bits to see what is missing to finish a proof step.

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 couldn't agree more.

Tobias


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



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