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
* "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