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 |
|
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 |
|
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 |
|
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. |
|
38 |
|
39 - The native font renderer of -Dapple.awt.graphics.UseQuartz=true |
|
40 fails to handle the infinitesimal font size of "hidden" text (e.g. |
|
41 used in Isabelle sub/superscripts). |
|
42 |
|
43 |
|
44 Known problems with OpenJDK |
|
45 =========================== |
|
46 |
|
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. |
|
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/ |
|