|
wenzelm@39855
|
1 |
<?xml version="1.0" encoding="ISO-8859-1" ?>
|
|
wenzelm@39855
|
2 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
|
|
wenzelm@39855
|
3 |
<html xmlns="http://www.w3.org/1999/xhtml">
|
|
wenzelm@39855
|
4 |
|
|
wenzelm@39855
|
5 |
<head>
|
|
wenzelm@39855
|
6 |
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
|
|
wenzelm@40031
|
7 |
<title>Notes on the Isabelle/jEdit Prover IDE</title>
|
|
wenzelm@39855
|
8 |
</head>
|
|
wenzelm@39855
|
9 |
|
|
wenzelm@39855
|
10 |
<body>
|
|
wenzelm@39855
|
11 |
|
|
wenzelm@40064
|
12 |
<h2>Notes on the Isabelle/jEdit Prover IDE</h2>
|
|
wenzelm@39855
|
13 |
|
|
wenzelm@39855
|
14 |
<ul>
|
|
wenzelm@39855
|
15 |
|
|
wenzelm@40031
|
16 |
<li>The original jEdit look-and-feel is generally preserved, although
|
|
wenzelm@40031
|
17 |
some default properties have been changed to accommodate Isabelle
|
|
wenzelm@41180
|
18 |
(e.g. the text area font).</li>
|
|
wenzelm@39855
|
19 |
|
|
wenzelm@40031
|
20 |
<li>Formal Isabelle/Isar text is checked asynchronously while editing.
|
|
wenzelm@40031
|
21 |
The user is in full command of the editor, and the prover refrains
|
|
wenzelm@40031
|
22 |
from locking portions of the buffer etc.</li>
|
|
wenzelm@40029
|
23 |
|
|
wenzelm@40031
|
24 |
<li>Prover feedback works via tooltips, syntax highlighting, colors,
|
|
wenzelm@40031
|
25 |
boxes etc. based on semantic markup provided by Isabelle in the
|
|
wenzelm@40031
|
26 |
background.</li>
|
|
wenzelm@40031
|
27 |
|
|
wenzelm@40031
|
28 |
<li>Using the mouse together with the modifier key <tt>C</tt>
|
|
wenzelm@40031
|
29 |
(<tt>CONTROL</tt> on Linux or Windows,
|
|
wenzelm@40029
|
30 |
<tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
|
|
wenzelm@40029
|
31 |
|
|
wenzelm@40031
|
32 |
<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
|
|
wenzelm@40031
|
33 |
windows by jEdit, which also allows multiple instances.</li>
|
|
wenzelm@39855
|
34 |
|
|
wenzelm@39855
|
35 |
</ul>
|
|
wenzelm@39855
|
36 |
|
|
wenzelm@41786
|
37 |
<h2>Limitations and workrounds (January 2011)</h2>
|
|
wenzelm@41786
|
38 |
|
|
wenzelm@41786
|
39 |
<ul>
|
|
wenzelm@41786
|
40 |
<li>No way to start/stop prover or switch to a different logic.<br/>
|
|
wenzelm@41786
|
41 |
<em>Workaround:</em> Change options and restart editor.</li>
|
|
wenzelm@41786
|
42 |
|
|
wenzelm@41786
|
43 |
<li>Multiple theory buffers cannot depend on each other, imports are
|
|
wenzelm@41786
|
44 |
resolved via the file-system.<br/>
|
|
wenzelm@41786
|
45 |
<em>Workaround:</em> Save/reload files manually.</li>
|
|
wenzelm@41786
|
46 |
|
|
wenzelm@41786
|
47 |
<li>No reclaiming of old/unused document versions in prover or
|
|
wenzelm@41786
|
48 |
editor.<br/>
|
|
wenzelm@41786
|
49 |
<em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
|
|
wenzelm@41786
|
50 |
|
|
wenzelm@41786
|
51 |
<li>Incremental reparsing sometimes produces unexpected command
|
|
wenzelm@41786
|
52 |
spans.<br/>
|
|
wenzelm@41786
|
53 |
<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
|
|
wenzelm@41786
|
54 |
|
|
wenzelm@41786
|
55 |
<li>Command execution sometimes gets stuck (purple background).<br/>
|
|
wenzelm@41786
|
56 |
<em>Workaround:</em> Force reparsing as above.</li>
|
|
wenzelm@41786
|
57 |
|
|
wenzelm@41786
|
58 |
<li>Odd behavior of some diagnostic commands, notably those
|
|
wenzelm@41786
|
59 |
starting external processes asynchronously
|
|
wenzelm@41786
|
60 |
(e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
|
|
wenzelm@41786
|
61 |
<em>Workaround:</em> Avoid such commands.</li>
|
|
wenzelm@41786
|
62 |
|
|
wenzelm@41786
|
63 |
<li>No support for non-local markup, e.g. commands reporting on
|
|
wenzelm@41786
|
64 |
previous commands (proof end on proof head), or markup produced by
|
|
wenzelm@41786
|
65 |
loading external files.</li>
|
|
wenzelm@41786
|
66 |
|
|
wenzelm@41786
|
67 |
<li>General lack of various conveniences known from Proof
|
|
wenzelm@41786
|
68 |
General.</li>
|
|
wenzelm@41786
|
69 |
</ul>
|
|
wenzelm@41786
|
70 |
|
|
wenzelm@39855
|
71 |
</body>
|
|
wenzelm@39855
|
72 |
</html>
|
|
wenzelm@39855
|
73 |
|