author | wenzelm |
Sun, 14 Nov 2010 17:33:28 +0100 | |
changeset 40537 | 8ac69a7960d3 |
parent 40519 | d02e483ee82a |
child 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 |
||
40519 | 18 |
Some limitations of the current implementation: |
37218 | 19 |
|
40519 | 20 |
* No provisions for theory file dependencies inside the editor. |
37218 | 21 |
|
22 |
* No reclaiming of old/unused document versions. Memory will fill |
|
23 |
up eventually, both on the JVM and ML side. |
|
24 |
||
25 |
* No support for non-local markup, e.g. commands reporting on |
|
26 |
previous commands (proof end on proof head), or markup produced by |
|
27 |
loading external files. |
|
28 |
||
29 |
* General lack of various conveniences known from Proof General. |
|
30 |
||
31 |
Despite these shortcomings, Isabelle/jEdit already demonstrates that |
|
32 |
interactive theorem proving can be much more than command-line |
|
33 |
interaction via TTY or editor front-ends (such as Proof General and |
|
34 |
its many remakes). |
|
35 |
||
36 |
||
37 |
Known problems with Mac OS |
|
38 |
========================== |
|
39 |
||
40 |
- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations, |
|
41 |
e.g. between the editor and the Console plugin, which is a standard |
|
42 |
swing text box. Similar for search boxes etc. |
|
43 |
||
37862 | 44 |
- ToggleButton selected state is not rendered if window focus is lost, |
45 |
which is probably a genuine feature of the Apple look-and-feel. |
|
46 |
||
37218 | 47 |
- Anti-aliasing does not really work as well as for Linux or Windows. |
48 |
(General Apple/Swing problem?) |
|
49 |
||
50 |
- Font.createFont mangles the font family of non-regular fonts, |
|
51 |
e.g. bold. IsabelleText font files need to be installed manually. |
|
52 |
||
37862 | 53 |
- Missing glyphs are collected from other fonts (like Emacs, Firefox). |
54 |
This is actually an advantage over the Oracle/Sun JVM on Windows or |
|
55 |
Linux, but probably also the deeper reason for the other oddities of |
|
56 |
Apple font management. |
|
37218 | 57 |
|
40156
ac648bedd5dc
back again to non-Apple font rendering (cf. 4977324373f2);
wenzelm
parents:
39245
diff
changeset
|
58 |
- 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
|
59 |
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
|
60 |
used in Isabelle sub/superscripts). |
ac648bedd5dc
back again to non-Apple font rendering (cf. 4977324373f2);
wenzelm
parents:
39245
diff
changeset
|
61 |
|
37218 | 62 |
|
40537 | 63 |
Known problems with OpenJDK |
64 |
=========================== |
|
37218 | 65 |
|
40537 | 66 |
- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of |
67 |
the jEdit text area. Always use official JRE 1.6.x from |
|
68 |
Sun/Oracle/Apple. |
|
37218 | 69 |
|
70 |
||
71 |
Licenses and home sites of contributing systems |
|
72 |
=============================================== |
|
73 |
||
74 |
* Scala: BSD-style |
|
75 |
http://www.scala-lang.org |
|
76 |
||
77 |
* jEdit: GPL (with special cases) |
|
78 |
http://www.jedit.org/ |
|
79 |
||
80 |
* Lobo/Cobra: GPL and LGPL |
|
81 |
http://lobobrowser.org/ |