Re: [isabelle] Isabelle2016-RC0 - default output buffers



On Thu, 7 Jan 2016, Tobias Nipkow wrote:

 I moved the current line cursor to a lemma statement.
 What I observed:
    The bottom buffer was set to output. It displays nothing
    The right buffer shows the Documentation panel.

 What I expected:
    The proof state is displayed somewhere.

 The proof state is only visible when I select the state panel (as
 documented). This might be confusing for new-comers.> In addition, my
 proof state is usually huge, but by default, the right panel is very
 small.

 Splitting state and output may be a good idea for power users with
 large displays. On my laptop with only one fullHD display, I just
 can't find a satisfying setting. Maybe it is a good idea to distribute
 Isabelle with a simple GUI setup. Power users can still change the
 defaults. This would mean that by default, the proof state is sent to
 the output panel.

 What do other users think?

I voiced the same concern when the new default was introduced.

Can you quote a changeset and mailing list message on that?

The State output has changed many times in the past few months. I have incorporated all observations and feedback into Isabelle2016-RC0 as far as I can tell.

If anything has been overlooked, I need concrete information on that.


	Makarius




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