|
wenzelm@41876
|
1 |
<?xml version="1.0" encoding="UTF-8" ?>
|
|
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@44341
|
7 |
<style type="text/css" media="screen">
|
|
wenzelm@44380
|
8 |
body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
|
|
wenzelm@44341
|
9 |
</style>
|
|
wenzelm@45983
|
10 |
<title>Welcome to the Isabelle/jEdit Prover IDE</title>
|
|
wenzelm@39855
|
11 |
</head>
|
|
wenzelm@39855
|
12 |
|
|
wenzelm@39855
|
13 |
<body>
|
|
wenzelm@39855
|
14 |
|
|
wenzelm@45984
|
15 |
<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
|
|
wenzelm@45577
|
16 |
|
|
wenzelm@45983
|
17 |
<p>
|
|
wenzelm@45984
|
18 |
<b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
|
|
wenzelm@45983
|
19 |
based on Isabelle/Scala technology that is integrated with Isabelle.
|
|
wenzelm@45983
|
20 |
It is build around a concept of
|
|
wenzelm@45983
|
21 |
<em>asynchronous document processing</em>, which is supported
|
|
wenzelm@45983
|
22 |
natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
|
|
wenzelm@45983
|
23 |
</p>
|
|
wenzelm@45983
|
24 |
|
|
wenzelm@45983
|
25 |
<p>
|
|
wenzelm@45983
|
26 |
<b>Isabelle/jEdit</b> is an example application within the PIDE
|
|
wenzelm@45983
|
27 |
framework — it illustrates many of the ideas in a realistic
|
|
wenzelm@45983
|
28 |
manner, ready to be used right now in Isabelle applications.
|
|
wenzelm@45983
|
29 |
</p>
|
|
wenzelm@45983
|
30 |
|
|
wenzelm@45983
|
31 |
<p>
|
|
wenzelm@45983
|
32 |
<em>Research and implementation of concepts around PIDE has been
|
|
wenzelm@45983
|
33 |
kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
|
|
wenzelm@45983
|
34 |
Université Paris-Sud (http://www.u-psud.fr), and Digiteo
|
|
wenzelm@45983
|
35 |
(http://www.digiteo.fr).</em>
|
|
wenzelm@45983
|
36 |
</p>
|
|
wenzelm@45983
|
37 |
|
|
wenzelm@45983
|
38 |
|
|
wenzelm@45983
|
39 |
|
|
wenzelm@45983
|
40 |
<h2>The Isabelle/jEdit Prover IDE</h2>
|
|
wenzelm@45983
|
41 |
|
|
wenzelm@45983
|
42 |
<p>
|
|
wenzelm@45983
|
43 |
Isabelle/jEdit consists of some plugins for the well-known jEdit text
|
|
wenzelm@45983
|
44 |
editor framework (http://www.jedit.org), according to the following
|
|
wenzelm@45983
|
45 |
principles.
|
|
wenzelm@45983
|
46 |
</p>
|
|
wenzelm@39855
|
47 |
|
|
wenzelm@39855
|
48 |
<ul>
|
|
wenzelm@39855
|
49 |
|
|
wenzelm@40031
|
50 |
<li>The original jEdit look-and-feel is generally preserved, although
|
|
wenzelm@40031
|
51 |
some default properties have been changed to accommodate Isabelle
|
|
wenzelm@41180
|
52 |
(e.g. the text area font).</li>
|
|
wenzelm@39855
|
53 |
|
|
wenzelm@40031
|
54 |
<li>Formal Isabelle/Isar text is checked asynchronously while editing.
|
|
wenzelm@40031
|
55 |
The user is in full command of the editor, and the prover refrains
|
|
wenzelm@40031
|
56 |
from locking portions of the buffer etc.</li>
|
|
wenzelm@40029
|
57 |
|
|
wenzelm@40031
|
58 |
<li>Prover feedback works via tooltips, syntax highlighting, colors,
|
|
wenzelm@40031
|
59 |
boxes etc. based on semantic markup provided by Isabelle in the
|
|
wenzelm@40031
|
60 |
background.</li>
|
|
wenzelm@40031
|
61 |
|
|
wenzelm@40031
|
62 |
<li>Using the mouse together with the modifier key <tt>C</tt>
|
|
wenzelm@40031
|
63 |
(<tt>CONTROL</tt> on Linux or Windows,
|
|
wenzelm@45982
|
64 |
<tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
|
|
wenzelm@40029
|
65 |
|
|
wenzelm@40031
|
66 |
<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
|
|
wenzelm@40031
|
67 |
windows by jEdit, which also allows multiple instances.</li>
|
|
wenzelm@39855
|
68 |
|
|
wenzelm@45983
|
69 |
<li>Prover process and source files are managed by the Scala layer on
|
|
wenzelm@45983
|
70 |
the editor side. The prover experiences a mostly timeless and
|
|
wenzelm@45983
|
71 |
stateless environment of formal document content.</li>
|
|
wenzelm@45983
|
72 |
|
|
wenzelm@39855
|
73 |
</ul>
|
|
wenzelm@39855
|
74 |
|
|
wenzelm@41876
|
75 |
|
|
wenzelm@41876
|
76 |
<h2>Isabelle symbols and fonts</h2>
|
|
wenzelm@41876
|
77 |
|
|
wenzelm@41876
|
78 |
<ul>
|
|
wenzelm@41876
|
79 |
<li>Isabelle supports infinitely many symbols:<br/>
|
|
wenzelm@44343
|
80 |
α, β, γ, …<br/>
|
|
wenzelm@44343
|
81 |
∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
|
|
wenzelm@44343
|
82 |
≤, ≥, ⊓, ⊔, …<br/>
|
|
wenzelm@44343
|
83 |
ℵ, △, ∇, …<br/>
|
|
wenzelm@44343
|
84 |
<tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/>
|
|
wenzelm@41876
|
85 |
</li>
|
|
wenzelm@41876
|
86 |
|
|
wenzelm@44341
|
87 |
<li>There are some special control symbols to modify the style of a
|
|
wenzelm@44341
|
88 |
<em>single</em> symbol:<br/>
|
|
wenzelm@44343
|
89 |
⇩ subscript<br/>
|
|
wenzelm@44343
|
90 |
⇧ superscript<br/>
|
|
wenzelm@44343
|
91 |
⇣ subscript within identifier<br/>
|
|
wenzelm@44343
|
92 |
⇡ superscript within identifier<br/>
|
|
wenzelm@44343
|
93 |
❙ bold face</li>
|
|
wenzelm@44341
|
94 |
|
|
wenzelm@41876
|
95 |
<li>A default mapping relates some Isabelle symbols to Unicode points
|
|
wenzelm@41876
|
96 |
(see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
|
|
wenzelm@41876
|
97 |
</li>
|
|
wenzelm@41876
|
98 |
|
|
wenzelm@41876
|
99 |
<li>The <em>IsabelleText</em> font ensures that Unicode points are actually
|
|
wenzelm@41876
|
100 |
seen on the screen (or printer).
|
|
wenzelm@41876
|
101 |
</li>
|
|
wenzelm@41876
|
102 |
|
|
wenzelm@41876
|
103 |
<li>Input methods:
|
|
wenzelm@41876
|
104 |
<ul>
|
|
wenzelm@41876
|
105 |
<li>copy/paste from decoded source files</li>
|
|
wenzelm@41876
|
106 |
<li>copy/paste from prover output</li>
|
|
wenzelm@41876
|
107 |
<li>completion provided by Isabelle plugin, e.g.<br/>
|
|
wenzelm@41876
|
108 |
|
|
wenzelm@41876
|
109 |
<table border="1">
|
|
wenzelm@41876
|
110 |
<tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr>
|
|
wenzelm@41876
|
111 |
|
|
wenzelm@44343
|
112 |
<tr><td>lambda</td> <td><tt>%</tt></td> <td>λ</td></tr>
|
|
wenzelm@44343
|
113 |
<tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr>
|
|
wenzelm@44343
|
114 |
<tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr>
|
|
wenzelm@41876
|
115 |
|
|
wenzelm@44343
|
116 |
<tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr>
|
|
wenzelm@44343
|
117 |
<tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr>
|
|
wenzelm@41876
|
118 |
|
|
wenzelm@44343
|
119 |
<tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr>
|
|
wenzelm@44343
|
120 |
<tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr>
|
|
wenzelm@44343
|
121 |
<tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr>
|
|
wenzelm@44343
|
122 |
<tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr>
|
|
wenzelm@44343
|
123 |
<tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr>
|
|
wenzelm@44343
|
124 |
<tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr>
|
|
wenzelm@44343
|
125 |
<tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr>
|
|
wenzelm@44343
|
126 |
<tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr>
|
|
wenzelm@44343
|
127 |
<tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr>
|
|
wenzelm@44341
|
128 |
|
|
wenzelm@44343
|
129 |
<tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr>
|
|
wenzelm@44343
|
130 |
<tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr>
|
|
wenzelm@44343
|
131 |
<tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr>
|
|
wenzelm@44343
|
132 |
<tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr>
|
|
wenzelm@44343
|
133 |
<tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr>
|
|
wenzelm@44341
|
134 |
|
|
wenzelm@41876
|
135 |
</table>
|
|
wenzelm@41876
|
136 |
</li>
|
|
wenzelm@41876
|
137 |
</ul>
|
|
wenzelm@41876
|
138 |
</li>
|
|
wenzelm@41876
|
139 |
|
|
wenzelm@41876
|
140 |
<li><b>NOTE:</b> The above abbreviations refer to the input method.
|
|
wenzelm@41876
|
141 |
The logical notation provides ASCII alternatives that often
|
|
wenzelm@41876
|
142 |
coincide, but deviate occasionally.
|
|
wenzelm@41876
|
143 |
</li>
|
|
wenzelm@41876
|
144 |
|
|
wenzelm@41876
|
145 |
<li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
|
|
wenzelm@41876
|
146 |
source replacement operations; this works for Isabelle as long
|
|
wenzelm@41876
|
147 |
as the Unicode sequences coincide with the symbol mapping.
|
|
wenzelm@41876
|
148 |
</li>
|
|
wenzelm@41876
|
149 |
|
|
wenzelm@45992
|
150 |
<li><b>NOTE:</b> Raw unicode characters within prover source files
|
|
wenzelm@45983
|
151 |
should be restricted to informal parts, e.g. to write text in
|
|
wenzelm@45983
|
152 |
non-latin alphabets. Mathematical symbols should be defined via the
|
|
wenzelm@45983
|
153 |
official rendering tables.
|
|
wenzelm@45983
|
154 |
</li>
|
|
wenzelm@45983
|
155 |
|
|
wenzelm@41876
|
156 |
</ul>
|
|
wenzelm@41876
|
157 |
|
|
wenzelm@41876
|
158 |
|
|
wenzelm@45992
|
159 |
<h2>Limitations and workrounds (October 2011)</h2>
|
|
wenzelm@41786
|
160 |
|
|
wenzelm@41786
|
161 |
<ul>
|
|
wenzelm@41786
|
162 |
<li>No way to start/stop prover or switch to a different logic.<br/>
|
|
wenzelm@41786
|
163 |
<em>Workaround:</em> Change options and restart editor.</li>
|
|
wenzelm@41786
|
164 |
|
|
wenzelm@41786
|
165 |
<li>Incremental reparsing sometimes produces unexpected command
|
|
wenzelm@41786
|
166 |
spans.<br/>
|
|
wenzelm@41786
|
167 |
<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
|
|
wenzelm@41786
|
168 |
|
|
wenzelm@45577
|
169 |
<li>Odd behavior of some diagnostic commands, notably those starting
|
|
wenzelm@45577
|
170 |
external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
|
|
wenzelm@45577
|
171 |
<em>Workaround:</em> Avoid such commands.</li>
|
|
wenzelm@41786
|
172 |
|
|
wenzelm@45577
|
173 |
<li>Lack of dependency managed for auxiliary files that contribute
|
|
wenzelm@45577
|
174 |
to a theory ("<b>uses</b>").<br/>
|
|
wenzelm@45577
|
175 |
<em>Workaround:</em> Re-use files manually within the prover.</li>
|
|
wenzelm@41786
|
176 |
|
|
wenzelm@45630
|
177 |
<li>Crude management of new Isar commands that are defined within
|
|
wenzelm@45630
|
178 |
the running session.<br/>
|
|
wenzelm@45630
|
179 |
<em>Workaround:</em> Force re-parsing of files using such commands
|
|
wenzelm@45630
|
180 |
via reload menu of jEdit.</li>
|
|
wenzelm@45630
|
181 |
|
|
wenzelm@45687
|
182 |
<li>No way to delete document nodes from the overall collection of
|
|
wenzelm@45687
|
183 |
theories.<br/>
|
|
wenzelm@45687
|
184 |
<em>Workaround:</em> Restart whole Isabelle/jEdit session in
|
|
wenzelm@45687
|
185 |
worst-case situation.</li>
|
|
wenzelm@45687
|
186 |
|
|
wenzelm@41786
|
187 |
<li>No support for non-local markup, e.g. commands reporting on
|
|
wenzelm@41786
|
188 |
previous commands (proof end on proof head), or markup produced by
|
|
wenzelm@41786
|
189 |
loading external files.</li>
|
|
wenzelm@41786
|
190 |
|
|
wenzelm@41786
|
191 |
<li>General lack of various conveniences known from Proof
|
|
wenzelm@41786
|
192 |
General.</li>
|
|
wenzelm@41786
|
193 |
</ul>
|
|
wenzelm@41786
|
194 |
|
|
wenzelm@45577
|
195 |
|
|
wenzelm@45982
|
196 |
<h2>Known problems with Mac OS X</h2>
|
|
wenzelm@45577
|
197 |
|
|
wenzelm@45577
|
198 |
<ul>
|
|
wenzelm@45577
|
199 |
|
|
wenzelm@45577
|
200 |
<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
|
|
wenzelm@45577
|
201 |
e.g. between the editor and the Console plugin, which is a standard
|
|
wenzelm@45577
|
202 |
swing text box. Similar for search boxes etc.</li>
|
|
wenzelm@45577
|
203 |
|
|
wenzelm@45982
|
204 |
<li><tt>Font.createFont</tt> mangles the font family of non-regular
|
|
wenzelm@45982
|
205 |
fonts, e.g. bold. IsabelleText font files need to be
|
|
wenzelm@45982
|
206 |
installed/updated manually if bold versions are desired. Note that
|
|
wenzelm@45982
|
207 |
this has to be repeated whenever fonts shipped with Isabelle are
|
|
wenzelm@45982
|
208 |
updated!</li>
|
|
wenzelm@45577
|
209 |
|
|
wenzelm@45577
|
210 |
<li>Missing glyphs are collected from other fonts (like Emacs,
|
|
wenzelm@45982
|
211 |
Firefox). This is actually an advantage over the Oracle JVM on
|
|
wenzelm@45982
|
212 |
Windows or Linux, but also the deeper reason for other oddities of
|
|
wenzelm@45982
|
213 |
Apple font management.</li>
|
|
wenzelm@45577
|
214 |
|
|
wenzelm@45982
|
215 |
<li>The native font renderer
|
|
wenzelm@45982
|
216 |
of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
|
|
wenzelm@45982
|
217 |
enabled by default) fails to handle the infinitesimal font size of
|
|
wenzelm@45982
|
218 |
"hidden" text (e.g. used in Isabelle sub/superscripts).</li>
|
|
wenzelm@45577
|
219 |
|
|
wenzelm@45577
|
220 |
</ul>
|
|
wenzelm@45577
|
221 |
|
|
wenzelm@45577
|
222 |
|
|
wenzelm@45577
|
223 |
<h2>Known problems with OpenJDK 1.6.x</h2>
|
|
wenzelm@45577
|
224 |
|
|
wenzelm@45577
|
225 |
<ul>
|
|
wenzelm@45577
|
226 |
|
|
wenzelm@45577
|
227 |
<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
|
|
wenzelm@45982
|
228 |
of the jEdit text area. Always use official JRE 1.6.x from Oracle
|
|
wenzelm@45982
|
229 |
or Apple.</li>
|
|
wenzelm@45577
|
230 |
|
|
wenzelm@45982
|
231 |
<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
|
|
wenzelm@45746
|
232 |
|
|
wenzelm@45746
|
233 |
</ul>
|
|
wenzelm@45746
|
234 |
|
|
wenzelm@45746
|
235 |
|
|
wenzelm@45577
|
236 |
<h2>Licenses and home sites of contributing systems</h2>
|
|
wenzelm@45577
|
237 |
|
|
wenzelm@45577
|
238 |
<ul>
|
|
wenzelm@45577
|
239 |
|
|
wenzelm@45983
|
240 |
<li>Isabelle: BSD-style</li>
|
|
wenzelm@45983
|
241 |
|
|
wenzelm@45577
|
242 |
<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
|
|
wenzelm@45577
|
243 |
|
|
wenzelm@45577
|
244 |
<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
|
|
wenzelm@45577
|
245 |
|
|
wenzelm@45577
|
246 |
<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
|
|
wenzelm@45577
|
247 |
|
|
wenzelm@45577
|
248 |
</ul>
|
|
wenzelm@45577
|
249 |
|
|
wenzelm@39855
|
250 |
</body>
|
|
wenzelm@39855
|
251 |
</html>
|