Re: [isabelle] 2014-RC1 issues

On Wed, 30 Jul 2014, Peter Lammich wrote:

The sidekick panel is supposed to show an overview of the theory.
At the top-level of the hierarchy, you can see the first lines of lemma,
definition, etc commands, which may or may not contain useful
information. In the worst case, you just see "lemma" or "definition".

It is even worse if you look under a lemma command. This looks like:
|- using
|- case
|- proof
|- apply
|- apply
|- done
|- qed

i.e., almost completely useless information.

The enumeration of the commands as "sections" is indeed a bit pointless.

The main use of Sidekick / isabelle is for document structure, with chapter / section / subsection outline etc. When writing Isabelle documentation, papers, slides etc. I use that routinely to keep an overview.

More logical structure could be done in many ways, I have this on my list for several years already to be revisited eventually.

The information that might be useful, i.e. the name and the proposition of the lemma, is displayed nowhere!

Depends how you write your source text. jEdit folds and Sidekick trees assume that the first line provides the main information. This is also the reason why I write definitions and theorem statements these days a bit differently than in the past, when Proof General was still there.

Of course, one could replace SideKick by a quite different Preview panel for the proof document with its relevant structural information, even proof state output according to certain policies of incremental editing of sub-proofs, not scripts. That is just speculative at the moment -- too many marginal technical problems still in the way of bigger steps forwards.


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