use exists_subterm directly;
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Isabelle support for jEdit -- http://www.jedit.org/
===================================================
This provides both a basic editing "mode" (with some degree of syntax
highlighting), and a minimal "plugin" with some support for
interaction with the Isabelle process.
Mode installation
-----------------
1) Copy or symlink [ISABELLE_HOME]/lib/jedit/isabelle.xml to
[JEDIT_SETTINGS]/modes/
2) Add the following entry [JEDIT_SETTINGS]/modes/catalog
<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>
Example catalog file:
<?xml version="1.0"?>
<!DOCTYPE MODES SYSTEM "catalog.dtd">
<MODES>
<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>
</MODES>
Plugin installation
-------------------
1) Install copies of the Isabelle jars:
[ISABELLE_HOME]/lib/classes/Pure.jar -> [JEDIT_SETTINGS]/jars/isabelle-Pure.jar
[ISABELLE_HOME]/lib/jedit/isabelle.jar -> [JEDIT_SETTINGS]/jars/isabelle.jar
2) Install scala-library.jar from the regular Scala distribution,
cf. the http://www.scala-lang.org/downloads/index.html as
[JEDIT_SETTINGS]/jars/isabelle-scala-library.jar
3) Enable the plugin using the manager of jEdit; invoke the "isabelle"
editor action. The resulting window may be docked, e.g. at bottom.
Note that the Errorlist plugin provides some useful options like "Show
error icons in the gutter", for immediate feedback of Isabelle
warnings and errors in the source text. The Errorlist window may be
docked likewise.
$Id$