|
1 <?xml version="1.0" encoding="UTF-8" ?> |
|
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
3 <html xmlns="http://www.w3.org/1999/xhtml"> |
|
4 |
|
5 <head> |
|
6 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> |
|
7 <title>Notes on the Isabelle/jEdit Prover IDE</title> |
|
8 </head> |
|
9 |
|
10 <body> |
|
11 |
|
12 <h2>The Isabelle/jEdit Prover IDE</h2> |
|
13 |
|
14 <ul> |
|
15 |
|
16 <li>The original jEdit look-and-feel is generally preserved, although |
|
17 some default properties have been changed to accommodate Isabelle |
|
18 (e.g. the text area font).</li> |
|
19 |
|
20 <li>Formal Isabelle/Isar text is checked asynchronously while editing. |
|
21 The user is in full command of the editor, and the prover refrains |
|
22 from locking portions of the buffer etc.</li> |
|
23 |
|
24 <li>Prover feedback works via tooltips, syntax highlighting, colors, |
|
25 boxes etc. based on semantic markup provided by Isabelle in the |
|
26 background.</li> |
|
27 |
|
28 <li>Using the mouse together with the modifier key <tt>C</tt> |
|
29 (<tt>CONTROL</tt> on Linux or Windows, |
|
30 <tt>COMMAND</tt> on Mac OS) exposes additional information.</li> |
|
31 |
|
32 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent |
|
33 windows by jEdit, which also allows multiple instances.</li> |
|
34 |
|
35 </ul> |
|
36 |
|
37 |
|
38 <h2>Isabelle symbols and fonts</h2> |
|
39 |
|
40 <ul> |
|
41 |
|
42 <li>Isabelle supports infinitely many symbols:<br/> |
|
43 α, β, γ, …<br/> |
|
44 ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/> |
|
45 ≤, ≥, ⊓, ⊔, …<br/> |
|
46 ℵ, △, ∇, …<br/> |
|
47 <tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/> |
|
48 </li> |
|
49 |
|
50 <li>A default mapping relates some Isabelle symbols to Unicode points |
|
51 (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>). |
|
52 </li> |
|
53 |
|
54 <li>The <em>IsabelleText</em> font ensures that Unicode points are actually |
|
55 seen on the screen (or printer). |
|
56 </li> |
|
57 |
|
58 <li>Input methods: |
|
59 <ul> |
|
60 <li>copy/paste from decoded source files</li> |
|
61 <li>copy/paste from prover output</li> |
|
62 <li>completion provided by Isabelle plugin, e.g.<br/> |
|
63 |
|
64 <table border="1"> |
|
65 <tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr> |
|
66 |
|
67 <tr><td>lambda</td> <td></td> <td>λ</td></tr> |
|
68 <tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr> |
|
69 <tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr> |
|
70 |
|
71 <tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr> |
|
72 <tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr> |
|
73 |
|
74 <tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr> |
|
75 <tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr> |
|
76 <tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr> |
|
77 <tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr> |
|
78 <tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr> |
|
79 <tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr> |
|
80 <tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr> |
|
81 <tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr> |
|
82 <tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr> |
|
83 </table> |
|
84 </li> |
|
85 </ul> |
|
86 </li> |
|
87 |
|
88 <li><b>NOTE:</b> The above abbreviations refer to the input method. |
|
89 The logical notation provides ASCII alternatives that often |
|
90 coincide, but deviate occasionally. |
|
91 </li> |
|
92 |
|
93 <li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar |
|
94 source replacement operations; this works for Isabelle as long |
|
95 as the Unicode sequences coincide with the symbol mapping. |
|
96 </li> |
|
97 |
|
98 </ul> |
|
99 |
|
100 |
|
101 <h2>Limitations and workrounds (January 2011)</h2> |
|
102 |
|
103 <ul> |
|
104 <li>No way to start/stop prover or switch to a different logic.<br/> |
|
105 <em>Workaround:</em> Change options and restart editor.</li> |
|
106 |
|
107 <li>Multiple theory buffers cannot depend on each other, imports are |
|
108 resolved via the file-system.<br/> |
|
109 <em>Workaround:</em> Save/reload files manually.</li> |
|
110 |
|
111 <li>No reclaiming of old/unused document versions in prover or |
|
112 editor.<br/> |
|
113 <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li> |
|
114 |
|
115 <li>Incremental reparsing sometimes produces unexpected command |
|
116 spans.<br/> |
|
117 <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li> |
|
118 |
|
119 <li>Command execution sometimes gets stuck (purple background).<br/> |
|
120 <em>Workaround:</em> Force reparsing as above.</li> |
|
121 |
|
122 <li>Odd behavior of some diagnostic commands, notably those |
|
123 starting external processes asynchronously |
|
124 (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/> |
|
125 <em>Workaround:</em> Avoid such commands.</li> |
|
126 |
|
127 <li>No support for non-local markup, e.g. commands reporting on |
|
128 previous commands (proof end on proof head), or markup produced by |
|
129 loading external files.</li> |
|
130 |
|
131 <li>General lack of various conveniences known from Proof |
|
132 General.</li> |
|
133 </ul> |
|
134 |
|
135 </body> |
|
136 </html> |
|
137 |