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

On Sun, 3 Jan 2016, C. Diekmann wrote:

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).

There are at least these ways to see the proof state:

  (1) Output panel with "Proof state" checkbox ticked (off by default)

  (2) State panel, after opening it in a standard way (according to the
     explanations in the jEdit or Isabelle/jEdit manuals, so
     Documentation *is* important, although not updated yet).

These variants roughly correspond to the "2-buffer model" versus "3-buffer model" of ancient Proof General times. It should be rather painless to switch back an forth between these modes, for people who care about that. I tend to use only (2) these days, and also explain it like that to new users.

This might be confusing for new-comers.

Why? Proof state is only secondary in Isar. It is possible to give several hours of Isabelle introduction without ever showing State (and Output). It depends a bit on the topic and the target audience, and on the mindset of the presenter how it is all done.

I normally show first the main text area, then its popups, then other things. Eventually also Output, State, Theories.

Unguided new-comers first see the main text buffer and the Documentation panel -- the latter now starts the clickable "Examples". We probably also need a guide to the remaining documentation -- maybe another example theory that uses the new @{doc} antiquotation.

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.

I've just checked again with a conventional 16x9 Full-HD 17" Laptop from 2013, using the default 18px font for the main text area. This immediately gives at least these options:

  (1) Main text is restricted to old-school 80 chars per line, and the
    right docking area (with State panel) is extended into the middle of
    the main window.

    Result: almost 50% screen size for State.

  (2) Main text area uses extended line length of 100 chars, and the right
    docking area is extended to 30-40% of main window size.

    Result: approx. 30-40% screen size for State, or approx. 50% if the
    output font scale is set to 85% (this can be done persistently with
    the Isabelle plugin option "Font Scale").

Younger people may also try smaller fonts for the main text and/or output.

It is also possible to make a floating instance of State, and put it on a separate physical screen. That is an investment of 100-200 EUR for hardware, and some desk space.

Maybe it is a good idea to distribute Isabelle with a simple GUI setup.

That was actually the intention of the arrangement of Isabelle2016-RC0. What can be simplified further?

I still need to update the Isabelle/jEdit manual in this respect, although I have the impression that most users avoid manuals as much as possible.

In addition there could be a nice introductory video. It is occasionally interesting to see what others have done, and what they find important to tell, e.g.


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