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