| author | wenzelm |
| Sat, 25 May 2013 17:40:44 +0200 | |
| changeset 52147 | 9943f8067f11 |
| parent 51621 | 8c0f6caba80e |
| child 53021 | d0fa3f446b9d |
| permissions | -rw-r--r-- |
| 41628 | 1 |
<?xml version="1.0" encoding="UTF-8" ?> |
| 39591 | 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"/> |
|
| 43470 | 7 |
<style type="text/css" media="screen"> |
| 49956 | 8 |
body { font-family: IsabelleText; font-size: 14pt; }
|
| 43470 | 9 |
</style> |
| 45098 | 10 |
<title>Welcome to the Isabelle/jEdit Prover IDE</title> |
| 39591 | 11 |
</head> |
12 |
||
13 |
<body> |
|
14 |
||
| 45099 | 15 |
<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center> |
| 45098 | 16 |
|
17 |
<p> |
|
| 51621 | 18 |
<b>PIDE</b> is a framework for Prover IDEs based on the |
19 |
Isabelle/Scala. It is built around a concept of |
|
| 45098 | 20 |
<em>asynchronous document processing</em>, which is supported |
| 51621 | 21 |
natively by the <em>parallel proof engine</em> that is implemented |
22 |
in Isabelle/ML. |
|
| 45098 | 23 |
</p> |
24 |
||
25 |
<p> |
|
| 51621 | 26 |
<b>Isabelle/jEdit</b> is the main example application of the PIDE |
27 |
framework — it is ready for small and large Isabelle |
|
28 |
applications, for beginners and experts alike. |
|
| 45098 | 29 |
</p> |
| 44700 | 30 |
|
| 45098 | 31 |
<p> |
| 47491 | 32 |
<em>Research and implementation of concepts around PIDE has started |
33 |
around 2008 and was kindly supported by BMBF (http://www.bmbf.de), |
|
|
48917
ce37d4f8b4f4
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
wenzelm
parents:
47741
diff
changeset
|
34 |
Université Paris-Sud (http://www.u-psud.fr), Digiteo |
|
ce37d4f8b4f4
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
wenzelm
parents:
47741
diff
changeset
|
35 |
(http://www.digiteo.fr), and ANR |
|
ce37d4f8b4f4
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
wenzelm
parents:
47741
diff
changeset
|
36 |
(http://www.agence-nationale-recherche.fr).</em> |
| 45098 | 37 |
</p> |
38 |
||
39 |
||
40 |
||
41 |
<h2>The Isabelle/jEdit Prover IDE</h2> |
|
42 |
||
43 |
<p> |
|
44 |
Isabelle/jEdit consists of some plugins for the well-known jEdit text |
|
45 |
editor framework (http://www.jedit.org), according to the following |
|
46 |
principles. |
|
47 |
</p> |
|
| 39591 | 48 |
|
49 |
<ul> |
|
50 |
||
| 51082 | 51 |
<li>The original jEdit look-and-feel is generally preserved, although some |
52 |
default properties have been changed to accommodate Isabelle (e.g. the text |
|
53 |
area font).</li> |
|
| 39736 | 54 |
|
| 51082 | 55 |
<li>Formal Isabelle/Isar text is checked asynchronously while editing. The |
56 |
user is in full command of the editor, and the prover refrains from locking |
|
57 |
portions of the buffer.</li> |
|
| 39591 | 58 |
|
| 51082 | 59 |
<li>Prover feedback works via colors, boxes, squiggly underline, |
60 |
hyperlinks, popup windows, icons, clickable output, all based on semantic |
|
61 |
markup produced by Isabelle in the background.</li> |
|
| 39738 | 62 |
|
| 51082 | 63 |
<li>Using the mouse together with the modifier key <tt>CONTROL</tt> (Linux, |
64 |
Windows) or <tt>COMMAND</tt> (Mac OS X) exposes additional formal |
|
65 |
content.</li> |
|
| 39736 | 66 |
|
| 51082 | 67 |
<li>Dockable panels (e.g. <em>Output</em>, <em>Symbols</em>) are managed as |
68 |
independent windows by jEdit, which also allows multiple instances.</li> |
|
| 39591 | 69 |
|
| 51082 | 70 |
<li>Formal output (in popups etc.) may be explored recursively, using the |
|
51049
0b48d00aba8f
minimal updated of jEdit/README.html, without any substantial reforms;
wenzelm
parents:
50544
diff
changeset
|
71 |
same techniques as in the editor source buffer.</li> |
|
0b48d00aba8f
minimal updated of jEdit/README.html, without any substantial reforms;
wenzelm
parents:
50544
diff
changeset
|
72 |
|
| 51082 | 73 |
<li>The prover process and source files are managed on the editor side. The |
74 |
prover operates on timeless and stateless document content via |
|
75 |
Isabelle/Scala.</li> |
|
76 |
||
77 |
<li>Plugin options of jEdit (for the <em>Isabelle</em> plugin) give access |
|
78 |
to a selection of Isabelle/Scala options and its persistence preferences, |
|
79 |
usually with immediate effect on the prover back-end or editor |
|
80 |
front-end.</li> |
|
81 |
||
82 |
<li>The logic image of the prover session may be specified within |
|
83 |
Isabelle/jEdit, but this requires restart. The new image is provided |
|
84 |
automatically by the Isabelle build process.</li> |
|
| 45098 | 85 |
|
| 39591 | 86 |
</ul> |
87 |
||
| 41628 | 88 |
|
89 |
<h2>Isabelle symbols and fonts</h2> |
|
90 |
||
91 |
<ul> |
|
92 |
<li>Isabelle supports infinitely many symbols:<br/> |
|
|
43472
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
93 |
α, β, γ, …<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
94 |
∀, ∃, ∨, ∧, ⟶, ⟷, …<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
95 |
≤, ≥, ⊓, ⊔, …<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
96 |
ℵ, △, ∇, …<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
97 |
<tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/> |
| 41628 | 98 |
</li> |
99 |
||
| 43470 | 100 |
<li>There are some special control symbols to modify the style of a |
101 |
<em>single</em> symbol:<br/> |
|
|
43472
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
102 |
⇩ subscript<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
103 |
⇧ superscript<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
104 |
⇣ subscript within identifier<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
105 |
⇡ superscript within identifier<br/> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
106 |
❙ bold face</li> |
| 43470 | 107 |
|
| 41628 | 108 |
<li>A default mapping relates some Isabelle symbols to Unicode points |
109 |
(see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>). |
|
110 |
</li> |
|
111 |
||
112 |
<li>The <em>IsabelleText</em> font ensures that Unicode points are actually |
|
113 |
seen on the screen (or printer). |
|
114 |
</li> |
|
115 |
||
116 |
<li>Input methods: |
|
117 |
<ul> |
|
|
51049
0b48d00aba8f
minimal updated of jEdit/README.html, without any substantial reforms;
wenzelm
parents:
50544
diff
changeset
|
118 |
<li>use the Symbols dockable</li> |
| 41628 | 119 |
<li>copy/paste from decoded source files</li> |
120 |
<li>copy/paste from prover output</li> |
|
121 |
<li>completion provided by Isabelle plugin, e.g.<br/> |
|
122 |
||
123 |
<table border="1"> |
|
124 |
<tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr> |
|
125 |
||
|
43472
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
126 |
<tr><td>lambda</td> <td><tt>%</tt></td> <td>λ</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
127 |
<tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
128 |
<tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr> |
| 41628 | 129 |
|
|
43472
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
130 |
<tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
131 |
<tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr> |
| 41628 | 132 |
|
|
43472
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
133 |
<tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
134 |
<tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
135 |
<tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
136 |
<tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
137 |
<tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
138 |
<tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
139 |
<tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
140 |
<tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
141 |
<tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr> |
| 43470 | 142 |
|
|
43472
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
143 |
<tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
144 |
<tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
145 |
<tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
146 |
<tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr> |
|
ac6db8f44e5d
literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents:
43470
diff
changeset
|
147 |
<tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr> |
| 43470 | 148 |
|
| 41628 | 149 |
</table> |
150 |
</li> |
|
151 |
</ul> |
|
152 |
</li> |
|
153 |
||
154 |
<li><b>NOTE:</b> The above abbreviations refer to the input method. |
|
155 |
The logical notation provides ASCII alternatives that often |
|
156 |
coincide, but deviate occasionally. |
|
157 |
</li> |
|
158 |
||
159 |
<li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar |
|
160 |
source replacement operations; this works for Isabelle as long |
|
161 |
as the Unicode sequences coincide with the symbol mapping. |
|
162 |
</li> |
|
163 |
||
| 51082 | 164 |
<li><b>NOTE:</b> Raw Unicode characters within prover source files |
| 45098 | 165 |
should be restricted to informal parts, e.g. to write text in |
166 |
non-latin alphabets. Mathematical symbols should be defined via the |
|
167 |
official rendering tables. |
|
168 |
</li> |
|
169 |
||
| 51082 | 170 |
<li><b>NOTE:</b> Control symbols may be applied to a region of selected |
171 |
text, either using the Symbols dockable or keyboard shortcuts.</li> |
|
172 |
||
| 41628 | 173 |
</ul> |
174 |
||
175 |
||
| 50544 | 176 |
<h2>Limitations and known problems</h2> |
|
41538
d060ccad02bd
updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents:
40894
diff
changeset
|
177 |
|
|
d060ccad02bd
updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents:
40894
diff
changeset
|
178 |
<ul> |
| 51082 | 179 |
<li>Keyboard shortcuts C-PLUS and C-MINUS for adjusting the editor font |
180 |
size depend on platform details and national keyboards.<br/> |
|
181 |
<em>Workaround: Use numeric keypad or rebind keys in the jEdit Shortcuts |
|
182 |
options dialog.</em></li> |
|
183 |
||
184 |
<li>Lack of dependency management for auxiliary files that contribute |
|
|
48917
ce37d4f8b4f4
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
wenzelm
parents:
47741
diff
changeset
|
185 |
to a theory (e.g. <tt>ML_file</tt>).<br/> |
|
ce37d4f8b4f4
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
wenzelm
parents:
47741
diff
changeset
|
186 |
<em>Workaround:</em> Re-load files manually within the prover.</li> |
|
41538
d060ccad02bd
updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents:
40894
diff
changeset
|
187 |
|
| 50544 | 188 |
<li>Odd behavior of some diagnostic commands with global |
189 |
side-effects, like writing a physical |
|
| 51111 | 190 |
file.<br/> |
191 |
<em>Workaround:</em> Avoid such commands.</li> |
|
| 50544 | 192 |
|
| 44806 | 193 |
<li>No way to delete document nodes from the overall collection of |
194 |
theories.<br/> |
|
195 |
<em>Workaround:</em> Restart whole Isabelle/jEdit session in |
|
196 |
worst-case situation.</li> |
|
197 |
||
| 51111 | 198 |
<li>Linux: some desktop environments with extreme animation effects |
199 |
may disrupt Java 7 window placement and keyboard focus.<br/> |
|
| 51082 | 200 |
<em>Workaround:</em> Disable such effects.</li> |
|
50131
921cc694057b
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
wenzelm
parents:
49956
diff
changeset
|
201 |
|
| 51111 | 202 |
<li>Linux: some X11 window managers that are not "re-parenting" |
203 |
cause problems with additional windows opened by the Java VM. This |
|
204 |
affects either historic or neo-minimalistic window managers like |
|
205 |
<em>awesome</em> or <em>xmonad</em>.<br/> |
|
|
51109
cabf63b1ddfd
Java assumes regular "re-parenting" window manager;
wenzelm
parents:
51082
diff
changeset
|
206 |
<em>Workaround:</em> Use regular re-parenting window manager.</li> |
|
cabf63b1ddfd
Java assumes regular "re-parenting" window manager;
wenzelm
parents:
51082
diff
changeset
|
207 |
|
| 51111 | 208 |
<li>Mac OS X: the native MacOSX plugin for jEdit tends to be |
209 |
disruptive and is off by default. Enabling it might or might not |
|
210 |
improve the user experience.<br/> |
|
| 51082 | 211 |
<em>Workaround:</em> Disable MacOSX plugin.</li></li> |
|
50131
921cc694057b
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
wenzelm
parents:
49956
diff
changeset
|
212 |
|
| 51111 | 213 |
<li>Mac OS X: Java 7 is officially supported on Lion and Mountain Lion, |
| 51082 | 214 |
but not Snow Leopard. It usually works on the latter, although with a |
215 |
small risk of instabilities.<br/> |
|
216 |
<em>Workaround:</em> Update to OS X Mountain Lion.</li> |
|
|
50131
921cc694057b
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
wenzelm
parents:
49956
diff
changeset
|
217 |
</ul> |
|
921cc694057b
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
wenzelm
parents:
49956
diff
changeset
|
218 |
|
|
921cc694057b
known problems with Mac OS X are back -- Java 7u6 is not the last word (cf. ce37d4f8b4f4);
wenzelm
parents:
49956
diff
changeset
|
219 |
|
| 44700 | 220 |
<h2>Licenses and home sites of contributing systems</h2> |
221 |
||
222 |
<ul> |
|
223 |
||
| 45098 | 224 |
<li>Isabelle: BSD-style</li> |
225 |
||
| 51082 | 226 |
<li>Poly/ML: LGPL <br/> http://www.polyml.org </li> |
227 |
||
| 44700 | 228 |
<li>Scala: BSD-style <br/> http://www.scala-lang.org</li> |
229 |
||
| 51082 | 230 |
<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org</li> |
| 44700 | 231 |
|
| 51082 | 232 |
<li>JFreeChart: LGPL <br/> http://www.jfree.org</li> |
233 |
||
234 |
<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org</li> |
|
| 44700 | 235 |
|
236 |
</ul> |
|
237 |
||
| 39591 | 238 |
</body> |
239 |
</html> |