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
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
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
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, http://plugins.jedit.org/plugins/?JythonInterpreter
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