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





On 03/01/2016 17:38, C. Diekmann wrote:
Hi,

when I first started RC0, the default setting was quite confusing for me.

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.

Tobias

Best Regards,
   Cornelius

2016-01-01 20:17 GMT+01:00 Makarius <makarius at sketis.net>:
Dear Isabelle users,

the coming Isabelle2016 release is scheduled for February 2016, after the
next big Java 8 update by Oracle in January and some weeks before the
deadline of ITP 2016.

To get started with systematic testing there is now the relatively early
http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding to
Isabelle/e18444532fce and AFP/c62777f3e932).

The website, NEWS, ANNOUNCE etc. are already mostly up-to-date.  Some
documentation is still lagging behind, notably the Isabelle/jEdit manual.
There are further fine points still to be sorted out.


When discussing problems, observations, suggustions, etc. the mail subject
line should be changed to something meaningful (but the release candidate
number still given in the message body).

As usual it is important to keep general laws of causality in mind: release
candidates may still change, but the final release is final. Although this
is tautological, in the past few releases we've often had complaints right
after final lift-off, when it was too late.

So the best time to start testing is now.


         Makarius



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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