Re: [isabelle] Feature suggestions: More useful output
On Fri, 23 Nov 2012, Joachim Breitner wrote:
Generally, I could imagine the output window being a bit more
informative, in particular with error messages.
For example, a failed "by method" currently just prints “Failed to
finish proof.” To fix this, I now have to change the "by" to "apply",
look at the result, fix it, and change it back. Could it not print
“Failed to finish proof. Remaining goals: ....”?
That is not a function of the output window, but of the prover to report
things in a certain way. During this summer, and now in fall moving
towards the coming winter release, I've made many refinements in both
areas, and hopefully manage to add 2-3 more rounds of refinement before
the next release. The general tendencies are like this:
(1) Output is becoming less and less important (it is an old TTY thing).
Instead the information is directly attached to the source. So the
messages are right there where things happen, while remaining
accessible in output for nostalgic reasons (for people who want to
make long moves with the mouse in the old way).
(2) Error feedback of Isar commands involving search/enumertion of
possibilities: this is an ancient issue from > 10 years ago, which I
have re-opened some weeks ago. So in the next release, you will see
proper errors for "by method", and the need to use 'apply' to imitate
that will be no longer there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and