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:
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and