src/Tools/jEdit/README

back again to non-Apple font rendering (cf. 4977324373f2);

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.
  http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf


Some limitations of the current implementation (as of Isabelle2009-2):

  * No provisions for editing multiple theory files.

  * No reclaiming of old/unused document versions.  Memory will fill
    up eventually, both on the JVM and ML side.

  * No support for non-local markup, e.g. commands reporting on
    previous commands (proof end on proof head), or markup produced by
    loading external files.

  * General lack of various conveniences known from Proof General.

Despite these shortcomings, Isabelle/jEdit already demonstrates that
interactive theorem proving can be much more than command-line
interaction via TTY or editor front-ends (such as Proof General and
its many remakes).


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 -Dapple.awt.graphics.UseQuartz=true
  fails to handle the infinitesimal font size of "hidden" text (e.g.
  used in Isabelle sub/superscripts).


Windows/Linux
=============

- Works best with Sun Java 1.6.x -- avoid OpenJDK for now.


Licenses and home sites of contributing systems
===============================================

* Scala: BSD-style
  http://www.scala-lang.org

* jEdit: GPL (with special cases)
  http://www.jedit.org/

* Lobo/Cobra: GPL and LGPL
  http://lobobrowser.org/


     Makarius
     31-May-2010