Re: [isabelle] Remaining reasons for Proof General
On Tue, 12 Nov 2013, Manuel Eberl wrote:
In this context, what is the point of "Sidekick"? It displays every
"have", every "using", every "by" as a single node?
There is no big point and it can be simply ignored. In 2010 I've made
some quick attempts to wire up Isabelle/jEdit with this generic jEdit
plugin and I did not find time yet to make it more serious. Its main
function at the moment is to provide some outline for section headings.
Occasional unfinished things are no remaining reason for Proof General,
especially since Proof General has nothing like SideKick at all.
I did make the completion serious in Isabelle2013-1, and it is no longer
This archive was generated by a fusion of
Pipermail (Mailman edition) and