author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 41538 d060ccad02bd
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;

Isabelle/jEdit based on Isabelle/Scala

The Isabelle/Scala layer that is already part of Isabelle/Pure
provides some general infrastructure for advanced prover interaction
and integration.  The Isabelle/jEdit application serves as an example
for asynchronous proof checking with support for parallel processing.

See also the paper:

  Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
  and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
  User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
  Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.

Known problems with Mac OS

- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
  e.g. between the editor and the Console plugin, which is a standard
  swing text box.  Similar for search boxes etc.

- ToggleButton selected state is not rendered if window focus is lost,
  which is probably a genuine feature of the Apple look-and-feel.

- Anti-aliasing does not really work as well as for Linux or Windows.
  (General Apple/Swing problem?)

- Font.createFont mangles the font family of non-regular fonts,
  e.g. bold.  IsabelleText font files need to be installed manually.

- Missing glyphs are collected from other fonts (like Emacs, Firefox).
  This is actually an advantage over the Oracle/Sun JVM on Windows or
  Linux, but probably also the deeper reason for the other oddities of
  Apple font management.

- The native font renderer of
  fails to handle the infinitesimal font size of "hidden" text (e.g.
  used in Isabelle sub/superscripts).

Known problems with OpenJDK

- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
  the jEdit text area.  Always use official JRE 1.6.x from

Licenses and home sites of contributing systems

* Scala: BSD-style

* jEdit: GPL (with special cases)

* Lobo/Cobra: GPL and LGPL