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">
6 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
7 <style type="text/css" media="screen">
8 body { font-family: IsabelleText; font-size: 14pt; }
10 <title>Welcome to the Isabelle/jEdit Prover IDE</title>
15 <center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
18 <b>PIDE</b> is a framework for sophisticated Prover IDEs,
19 based on Isabelle/Scala technology that is integrated with Isabelle.
20 It is built around a concept of
21 <em>asynchronous document processing</em>, which is supported
22 natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
26 <b>Isabelle/jEdit</b> is the flagship application of the PIDE
27 framework — it illustrates many of the ideas in a realistic
28 manner, ready to be used right now in Isabelle applications.
32 <em>Research and implementation of concepts around PIDE has started
33 around 2008 and was kindly supported by BMBF (http://www.bmbf.de),
34 Université Paris-Sud (http://www.u-psud.fr), Digiteo
35 (http://www.digiteo.fr), and ANR
36 (http://www.agence-nationale-recherche.fr).</em>
41 <h2>The Isabelle/jEdit Prover IDE</h2>
44 Isabelle/jEdit consists of some plugins for the well-known jEdit text
45 editor framework (http://www.jedit.org), according to the following
51 <li>The original jEdit look-and-feel is generally preserved, although
52 some default properties have been changed to accommodate Isabelle
53 (e.g. the text area font).</li>
55 <li>Formal Isabelle/Isar text is checked asynchronously while editing.
56 The user is in full command of the editor, and the prover refrains
57 from locking portions of the buffer etc.</li>
59 <li>Prover feedback works via tooltips, syntax highlighting, colors,
60 boxes etc. based on semantic markup provided by Isabelle in the
63 <li>Using the mouse together with the modifier key <tt>C</tt>
64 (<tt>CONTROL</tt> on Linux or Windows,
65 <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
67 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent
68 windows by jEdit, which also allows multiple instances.</li>
70 <li>Formal output (tooltips etc.) may be explored recursively, using the
71 same techniques as in the editor source buffer.</li>
73 <li>Prover process and source files are managed by the Isabelle/Scala on
74 the editor side. The prover experiences a mostly timeless and
75 stateless environment of formal document content.</li>
80 <h2>Isabelle symbols and fonts</h2>
83 <li>Isabelle supports infinitely many symbols:<br/>
85 ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
88 <tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/>
91 <li>There are some special control symbols to modify the style of a
92 <em>single</em> symbol:<br/>
95 ⇣ subscript within identifier<br/>
96 ⇡ superscript within identifier<br/>
99 <li>A default mapping relates some Isabelle symbols to Unicode points
100 (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
103 <li>The <em>IsabelleText</em> font ensures that Unicode points are actually
104 seen on the screen (or printer).
109 <li>use the Symbols dockable</li>
110 <li>copy/paste from decoded source files</li>
111 <li>copy/paste from prover output</li>
112 <li>completion provided by Isabelle plugin, e.g.<br/>
115 <tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr>
117 <tr><td>lambda</td> <td><tt>%</tt></td> <td>λ</td></tr>
118 <tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr>
119 <tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr>
121 <tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr>
122 <tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr>
124 <tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr>
125 <tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr>
126 <tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr>
127 <tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr>
128 <tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr>
129 <tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr>
130 <tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr>
131 <tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr>
132 <tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr>
134 <tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr>
135 <tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr>
136 <tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr>
137 <tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr>
138 <tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr>
145 <li><b>NOTE:</b> The above abbreviations refer to the input method.
146 The logical notation provides ASCII alternatives that often
147 coincide, but deviate occasionally.
150 <li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
151 source replacement operations; this works for Isabelle as long
152 as the Unicode sequences coincide with the symbol mapping.
155 <li><b>NOTE:</b> Raw unicode characters within prover source files
156 should be restricted to informal parts, e.g. to write text in
157 non-latin alphabets. Mathematical symbols should be defined via the
158 official rendering tables.
164 <h2>Limitations and known problems</h2>
167 <li>Lack of dependency managed for auxiliary files that contribute
168 to a theory (e.g. <tt>ML_file</tt>).<br/>
169 <em>Workaround:</em> Re-load files manually within the prover.</li>
171 <li>Odd behavior of some diagnostic commands with global
172 side-effects, like writing a physical
173 file.<br/> <em>Workaround:</em> Avoid such commands.</li>
175 <li>No way to delete document nodes from the overall collection of
177 <em>Workaround:</em> Restart whole Isabelle/jEdit session in
178 worst-case situation.</li>
180 <li>No support for non-local markup, e.g. commands reporting on
181 previous commands (proof end on proof head), or markup produced by
182 loading external files.</li>
184 <li>The native MacOSX plugin for jEdit tends to be disruptive. It
185 might or might not improve the user experience, and is off by
188 <li>Java 7 on MacOSX is officially supported on Lion and Mountain
189 Lion, but not Snow Leopard. It usually works on the latter, but
190 there might be some instabilities.</li>
194 <h2>Licenses and home sites of contributing systems</h2>
198 <li>Isabelle: BSD-style</li>
200 <li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
202 <li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
204 <li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>