[isabelle-dev] superfluous [?]

[Makarius]

On Wed, 10 Oct 2012, Peter Lammich wrote:

> It's always problematic if the user cannot be sure whether his theorem 
> is actually proved, or the proof method is just diverging in a parallel 
> thread. Thus, a UI should provide very clear information to the user, 
> otherwise we will get "Problem" reports of the form: "Everything runs 
> fine in JEdit, but when building the session via command line it 
> computes for 10 minutes and then fails ..."

So have you tried Isabelle/jEdit in the meantime?  As part of the 
parallelization of terminal proofs there is much more red in the text than 
before.


See also the recent "quick and dirty" thread: 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-October/msg00003.html

This motivates again why different behaviour in different "modes" causes 
confusion about what the system might be doing.

BTW, the [?] printing can be avoided by enabling quick_and_dirty mode, 
what Proof General normally does.


 	Makarius