Extending Isabelle/jEdit

jEdit's macro mechanism can be used to provide additional commands and features for Isabelle/jEdit. We hereby provide a collection of macros and other extensions and explain how to use it.

Installation

• Add this to your "$ISABELLE_HOME_USER/etc/settings" file:

init_component "$ISABELLE_HOME_USER/contrib/jedit-macros2013"

• Download the component (if this step fails on Windows/Cygwin, download the .tar.gz manually to the directory contrib):

isabelle components -a -R http://bitbucket.org/immler/isabelle-jedit-macros/downloads

• Install the macros

isabelle macros

• (Re)start Isabelle/jEdit

isabelle jedit

Macros

After installation, the following macros appear in a separate menu (Macros->Isabelle) and keyboard shortcuts can be mapped to Macros (Utilities->Options->Shortcuts).

• insertion of textual commands -- an attempt to simulate some of PG's menu items
  • find_theorems
  • sledgehammer
  • print_cases
  • ...

• Dialog box for find_theorems
  • automatically removes the command from the document
  • allows to detach results

• Experimental macros (they do not use an official interface to Isabelle/jEdit)
  • toggle "Auto Update", "Update" and "Detach" in the docked Output-window
  • stop/restart checking: allows to (temporarily) stop checking the documents; if you are stressed by over-eager checking of the prover

Additional Features

These features are enabled automatically:

• display the name of the loaded logic in jEdit's titlebar

• provide a widget which displays the loaded logic in jEdit's statusbar
  • can be added via Utilities->Options->Status Bar->Widgets, with the name "IsabelleLogic"

Disclaimer

Some of the macros and additional features are hacky, experimental, and do not use an official interface to Isabelle/jEdit! They could stop working with any new version!

Motivation

Using jEdit's macro mechanism it is fairly easy to customize jEdit to a certain extent, without throwing long lists of feature requests at developers. The community itself can create and improve extensions and everything is noninvasive in the sense that those who wish to use the extended functionality can easily do so, while the basic Isabelle plugin keeps pristine. Maybe some extensions are so successful that they will be incorporated in the official release at some point. But the point is, we have the chance to knock together whatever we like and maybe it turns out to be useful for others as well. — Christian Sternagel (talk)

Contributions

Macros were written by Christian Sternagel and Fabian Immler.

A repository for the collection of Macros is hosted at [1].

If you want to report issues, make suggestions, or contribute, please contact Fabian (immlerATin.tum.de).