Re: [isabelle] Isabelle's jEdit plugin: some known help documents?

On 7/31/2012 10:25 AM, Yannick Duchêne (Hibou57) wrote:
Any body know a location for the Isabelle plugin for jEdit help?


I've never seen an Isabelle plugin help. All the helps for plugins show up under the "Plugins" tree of "Help / jEdit help". Like Emacs, most of what pertains to using jEdit isn't specific to Isabelle.

I feel the Isabelle community favors Emacs's ProofGeneral over jEdit (or I may be wrong), and feel there are fewer documents for Isabelle used with jEdit.

I think the commitment has already been made that jEdit is the future. Emacs lovers can only savor the present, and long for the past in the future. I'd get philosophical about all the pros and cons, but it's a mute point. Lots of things are decided for us by the developers.

If you get used to jEdit, you'll find out that, like Emacs, it's very powerful, user configurable, has a powerful scripting language, and has lots of great plugins. Not having got tied into Emacs, ignorance is bliss for me.

As to how you use jEdit is used with Isabelle, at this point, Isabelle's operation with jEdit is fairly streamlined. There's the edit buffer, the output panel to show you current proof information, sidekick to give you a tree view, and the continuous prover which is always on.

To control all of that, there's essentially the Isar language, and knowing Isar will get you most of what Emacs makes available through menus.

Menus are nice to show you what's available, but it's not all upside when I go 3 levels deep in a menu and see 40 items available that I know nothing about.

With jEdit, anything that's available as na Isar command, you can make into a menu item and keyborad shortcut with jEdit macros. In fact, any macro you put under ".isabell/Isabelle2012/jedit/macros" will show up under the menu "Macros" in the toolbar.

For example, I have a macro "declare[[show_types=false]].bsh", which contains:


And I have a keyboard shortcut of "Cntl-j-i-t". You assign keyboard shorcuts to macros with "Plugin options / jEdit / Shortcuts".

That's how I was doing things. Now I put a bunch of commands in a file I import, like:

  declare[[show_brackets=true]]  declare[[show_types=true]]
  declare[[names_long=false]]    declare[[show_sorts=false]]
  declare[[names_unique=true]]   declare[[show_consts=true]]

Like with Emacs, there's lots of ways to do things. If you know how to use Isar, then you can get most of the same thing. As far as setting trace depth, I haven't found anything about that.

Some of the these features will get worked out. From my research, there's no one else close to Isabelle, what with Isar, jEdit, and powerful tools like Sledgehammer and Nitpick.

The jEdit plugins are powerful.

The "Console" plugin comes by default. I'm starting to use that because I get into the same Cygwin environment that jEdit is using. It also makes it easy to execute commands on the current buffer.

jEdit also has a standard scripting language, Beanshell, and so you get a standard scripting language with the power of Java. I'm also using the Jython plugin,

That will let you tie into Beanshell, and a Jython script can be run as a jEdit macro. I get the benefits of Python and Beanshell.

All together it's powerful. Learning it's a pain, but there's always a learning curve to these things.


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