src/Tools/jEdit/README
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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     1
Isabelle/jEdit based on Isabelle/Scala
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     2
======================================
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     3
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     4
The Isabelle/Scala layer that is already part of Isabelle/Pure
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     5
provides some general infrastructure for advanced prover interaction
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     6
and integration.  The Isabelle/jEdit application serves as an example
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     7
for asynchronous proof checking with support for parallel processing.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     8
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
     9
See also the paper:
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    10
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    11
  Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    12
  and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    13
  User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    14
  Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    15
  http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    16
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    17
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    18
Known problems with Mac OS
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    19
==========================
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    20
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    21
- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    22
  e.g. between the editor and the Console plugin, which is a standard
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    23
  swing text box.  Similar for search boxes etc.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    24
37862
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    25
- ToggleButton selected state is not rendered if window focus is lost,
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    26
  which is probably a genuine feature of the Apple look-and-feel.
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    27
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    28
- Anti-aliasing does not really work as well as for Linux or Windows.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    29
  (General Apple/Swing problem?)
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    30
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    31
- Font.createFont mangles the font family of non-regular fonts,
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    32
  e.g. bold.  IsabelleText font files need to be installed manually.
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    33
37862
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    34
- Missing glyphs are collected from other fonts (like Emacs, Firefox).
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    35
  This is actually an advantage over the Oracle/Sun JVM on Windows or
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    36
  Linux, but probably also the deeper reason for the other oddities of
ec81023c6861 further Mac OS X deviations;
wenzelm
parents: 37218
diff changeset
    37
  Apple font management.
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    38
40156
ac648bedd5dc back again to non-Apple font rendering (cf. 4977324373f2);
wenzelm
parents: 39245
diff changeset
    39
- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
ac648bedd5dc back again to non-Apple font rendering (cf. 4977324373f2);
wenzelm
parents: 39245
diff changeset
    40
  fails to handle the infinitesimal font size of "hidden" text (e.g.
ac648bedd5dc back again to non-Apple font rendering (cf. 4977324373f2);
wenzelm
parents: 39245
diff changeset
    41
  used in Isabelle sub/superscripts).
ac648bedd5dc back again to non-Apple font rendering (cf. 4977324373f2);
wenzelm
parents: 39245
diff changeset
    42
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    43
40537
8ac69a7960d3 updated README;
wenzelm
parents: 40519
diff changeset
    44
Known problems with OpenJDK
8ac69a7960d3 updated README;
wenzelm
parents: 40519
diff changeset
    45
===========================
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    46
40537
8ac69a7960d3 updated README;
wenzelm
parents: 40519
diff changeset
    47
- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
8ac69a7960d3 updated README;
wenzelm
parents: 40519
diff changeset
    48
  the jEdit text area.  Always use official JRE 1.6.x from
8ac69a7960d3 updated README;
wenzelm
parents: 40519
diff changeset
    49
  Sun/Oracle/Apple.
37218
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    50
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    51
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    52
Licenses and home sites of contributing systems
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    53
===============================================
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    54
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    55
* Scala: BSD-style
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    56
  http://www.scala-lang.org
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    57
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    58
* jEdit: GPL (with special cases)
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    59
  http://www.jedit.org/
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    60
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    61
* Lobo/Cobra: GPL and LGPL
ffd587207d5d notes on Isabelle/jEdit;
wenzelm
parents:
diff changeset
    62
  http://lobobrowser.org/