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

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

Best Regards,
  Cornelius




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