Re: [isabelle] Isabelle2016-RC0 - default output buffers
2016-01-03 22:51 GMT+01:00 Makarius <makarius at sketis.net>:
> 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
> 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.
It is painless. I can confirm that ;-)
I just documented why I was baffled on the first start. Maybe I still
live in the apply-style world.
>> 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.
Maybe I also need such an introduction. I'm using Isabelle for some
years now and learned many new things when I attended one of your
short introduction talks. In particular, the trend to move away from
`declare[[everything]]` and get the result in the output buffer
towards ctrl+hover everything. Thanks.
>> 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. https://www.youtube.com/watch?v=QYbAmRY1C5A
Actually, I did not get the intention behind the GUI until now.
Probably there should be a "what is new and fancy in Isabelle2016"
video. For technical details, I still prefer the written
This archive was generated by a fusion of
Pipermail (Mailman edition) and