10 <title>Notes on the Isabelle/jEdit Prover IDE</title> |
10 <title>Notes on the Isabelle/jEdit Prover IDE</title> |
11 </head> |
11 </head> |
12 |
12 |
13 <body> |
13 <body> |
14 |
14 |
15 <h2>The Isabelle/jEdit Prover IDE</h2> |
15 <h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2> |
|
16 |
|
17 The Isabelle/Scala layer that is already part of Isabelle/Pure |
|
18 provides some general infrastructure for advanced prover interaction |
|
19 and integration. The Isabelle/jEdit application serves as an example |
|
20 for asynchronous proof checking with support for parallel processing. |
16 |
21 |
17 <ul> |
22 <ul> |
18 |
23 |
19 <li>The original jEdit look-and-feel is generally preserved, although |
24 <li>The original jEdit look-and-feel is generally preserved, although |
20 some default properties have been changed to accommodate Isabelle |
25 some default properties have been changed to accommodate Isabelle |
114 </li> |
119 </li> |
115 |
120 |
116 </ul> |
121 </ul> |
117 |
122 |
118 |
123 |
119 <h2>Limitations and workrounds (January 2011)</h2> |
124 <h2>Limitations and workrounds (September 2011)</h2> |
120 |
125 |
121 <ul> |
126 <ul> |
122 <li>No way to start/stop prover or switch to a different logic.<br/> |
127 <li>No way to start/stop prover or switch to a different logic.<br/> |
123 <em>Workaround:</em> Change options and restart editor.</li> |
128 <em>Workaround:</em> Change options and restart editor.</li> |
124 |
|
125 <li>Limited support for dependencies between multiple theory buffers.<br/> |
|
126 <em>Workaround:</em> Load required files manually.</li> |
|
127 |
|
128 <li>No reclaiming of old/unused document versions in prover or |
|
129 editor.<br/> |
|
130 <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li> |
|
131 |
129 |
132 <li>Incremental reparsing sometimes produces unexpected command |
130 <li>Incremental reparsing sometimes produces unexpected command |
133 spans.<br/> |
131 spans.<br/> |
134 <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li> |
132 <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li> |
135 |
133 |
136 <li>Command execution sometimes gets stuck (purple background).<br/> |
134 <li>Odd behavior of some diagnostic commands, notably those starting |
137 <em>Workaround:</em> Force reparsing as above.</li> |
135 external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/> |
138 |
|
139 <li>Odd behavior of some diagnostic commands, notably those |
|
140 starting external processes asynchronously |
|
141 (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/> |
|
142 <em>Workaround:</em> Avoid such commands.</li> |
136 <em>Workaround:</em> Avoid such commands.</li> |
|
137 |
|
138 <li>Lack of dependency managed for auxiliary files that contribute |
|
139 to a theory ("<b>uses</b>").<br/> |
|
140 <em>Workaround:</em> Re-use files manually within the prover.</li> |
143 |
141 |
144 <li>No support for non-local markup, e.g. commands reporting on |
142 <li>No support for non-local markup, e.g. commands reporting on |
145 previous commands (proof end on proof head), or markup produced by |
143 previous commands (proof end on proof head), or markup produced by |
146 loading external files.</li> |
144 loading external files.</li> |
147 |
145 |
148 <li>General lack of various conveniences known from Proof |
146 <li>General lack of various conveniences known from Proof |
149 General.</li> |
147 General.</li> |
150 </ul> |
148 </ul> |
151 |
149 |
|
150 |
|
151 <h2>Known problems with Mac OS</h2> |
|
152 |
|
153 <ul> |
|
154 |
|
155 <li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations, |
|
156 e.g. between the editor and the Console plugin, which is a standard |
|
157 swing text box. Similar for search boxes etc.</li> |
|
158 |
|
159 <li>ToggleButton selected state is not rendered if window focus is |
|
160 lost, which is probably a genuine feature of the Apple |
|
161 look-and-feel.</li> |
|
162 |
|
163 <li>Font.createFont mangles the font family of non-regular fonts, |
|
164 e.g. bold. IsabelleText font files need to be installed/updated |
|
165 manually.</li> |
|
166 |
|
167 <li>Missing glyphs are collected from other fonts (like Emacs, |
|
168 Firefox). This is actually an advantage over the Oracle/Sun JVM on |
|
169 Windows or Linux, but probably also the deeper reason for the other |
|
170 oddities of Apple font management.</li> |
|
171 |
|
172 <li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true |
|
173 (not enabled by default) fails to handle the infinitesimal font size |
|
174 of "hidden" text (e.g. used in Isabelle sub/superscripts).</li> |
|
175 |
|
176 </ul> |
|
177 |
|
178 |
|
179 <h2>Known problems with OpenJDK 1.6.x</h2> |
|
180 |
|
181 <ul> |
|
182 |
|
183 <li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance |
|
184 of the jEdit text area. Always use official JRE 1.6.x from |
|
185 Sun/Oracle/Apple.</li> |
|
186 |
|
187 <li>jEdit on OpenJDK is generally not supported.</li> |
|
188 |
|
189 </ul> |
|
190 |
|
191 |
|
192 <h2>Licenses and home sites of contributing systems</h2> |
|
193 |
|
194 <ul> |
|
195 |
|
196 <li>Scala: BSD-style <br/> http://www.scala-lang.org</li> |
|
197 |
|
198 <li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li> |
|
199 |
|
200 <li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li> |
|
201 |
|
202 </ul> |
|
203 |
152 </body> |
204 </body> |
153 </html> |
205 </html> |
154 |
|