Re: [isabelle] New error messages in Isabelle 2013

On Wed, 30 Jan 2013, Alfio Martini wrote:

I sent you [yesterday] the file error_test.thy so you could see more precisely what is really making me feel uncomfortable with this. Maybe is a lack of proper interpretation of the message displayed in the output window from my part. I attach here again an image that shows the situation. I would expect the output window to show exactly what appears in the tooltip window. Nothing more than this. What is shown in the tooltip window is fine. On the other hand, what is shown in the output seems to be highly ambiguous to me.

The Output panel gives you a full record of all messages emitted by some command transaction, essentially as a fall-back for the traditional model, to avoid surprises that some tools don't get their information through.

This also explains its redundancy for this "by" step that concludes a "show":

  * "Succesful attempt ..."

  * Succesful proof state after it

  * Unsuccessful proof state from the forked proof

Attaching more messages to the place where they belong statically, not dynamically should clarify this further.

Mentally, it might help to understand "Output is machine state", and be tolerant for more internal tracing happening there than in the document model as visualized in the source.

It seems that in this situation the slight reforms of the Prover IDE were not going far enough, but such things cannot be changed in a rash manner.


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