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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and