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


	Makarius




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