Re: [isabelle] RC-3 puts method error after subgoals and warnings in output
Am 13.08.14 19:59, schrieb Makarius:
In PIDE the annotated source is the primary means of exposing prover
In contrast, the Output dockable is not really part of the PIDE
concepts. It is still around as a fall-back to display proof states,
and anything else concatenated in some canonical order given
implicitly by the prover. Thus Output is merely an intermediate
approximation of the real thing, which would probably be the
speculative "Preview" panel to show the document sources with
intermediate proof states, according to what is presently relevant in
the structured proof editing.
I am using myself Output relatively rarely. In the Isabelle tutorial
this Spring there was a funny incident: after approx. 2h explaining
Isabelle proof document editing, with various examples of definitions
and proofs, Timothy Bourke pointed out that I should also show the
Output panel for message display. I had just forgotten that, because
it was not necessary up to that point. But he was right that beginners
often manage more quickly to operate the Output panel than the
delicate choreography with the mouse that is required for hovering.
The latter is more flexible after some practice, though.
Here's some experience from a course we gave last year:
We had some students that were output panel agnostic. They developed no
understanding at all about the proof state and why things didn't work as
expected. E.g. you can't simply assume ~A and show False. They had
problems with including assumptions in inductions, as for them they were
obviously part of the proof as the document explicitly stated them. The
difference in this apparent redundancy is hard to grasp from the
document without consulting the output. Also the ability to just
continue editing and getting things evaluated after many errors together
with the agnostic for the proof state lead to "nearly done proofs" that
were merely accumulations of loosely connected statements.
I don't know if these problems were always there and students ignored
the output in PG as well but I think the PIDE fosters this behaviour.
This archive was generated by a fusion of
Pipermail (Mailman edition) and