On 08/01/2016 16:36, Makarius wrote:
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
Description: S/MIME Cryptographic Signature