Re: [isabelle] PIDE Display of Assumptions



On Fri, 29 Jun 2012, Makarius wrote:

On Fri, 29 Jun 2012, Patrick Michel wrote:

While updating my theories to Isabelle/HOL 2012 (worked like a charm) I was also trying out PIDE. I am quite happy with the IDE so far, once I figured out how to search for theorems, etc.

See the isar-ref manual for all commands. The 'help' command also gives you a complete list.

Even more obvious: use the command completion. You type "find" and wait 300ms and get a selection of find commands. Same for "print" or whatever you please, e.g. "sl" for "sledgehammer".

You can also modify the reactivity of the completion popup in the Plugin Options for SideKick in jEdit. (In Isabelle2012 it is a bit more ambitious than in Isabelle2011-1, but still not as aggressive as it can be for full virtuosity of jEdit experts.)


	Makarius





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