<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<style type="text/css" media="screen">
body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
</style>
<title>Welcome to the Isabelle/jEdit Prover IDE</title>
</head>
<body>
<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
<p>
<b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
based on Isabelle/Scala technology that is integrated with Isabelle.
It is build around a concept of
<em>asynchronous document processing</em>, which is supported
natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
</p>
<p>
<b>Isabelle/jEdit</b> is an example application within the PIDE
framework — it illustrates many of the ideas in a realistic
manner, ready to be used right now in Isabelle applications.
</p>
<p>
<em>Research and implementation of concepts around PIDE has been
kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
Université Paris-Sud (http://www.u-psud.fr), and Digiteo
(http://www.digiteo.fr).</em>
</p>
<h2>The Isabelle/jEdit Prover IDE</h2>
<p>
Isabelle/jEdit consists of some plugins for the well-known jEdit text
editor framework (http://www.jedit.org), according to the following
principles.
</p>
<ul>
<li>The original jEdit look-and-feel is generally preserved, although
some default properties have been changed to accommodate Isabelle
(e.g. the text area font).</li>
<li>Formal Isabelle/Isar text is checked asynchronously while editing.
The user is in full command of the editor, and the prover refrains
from locking portions of the buffer etc.</li>
<li>Prover feedback works via tooltips, syntax highlighting, colors,
boxes etc. based on semantic markup provided by Isabelle in the
background.</li>
<li>Using the mouse together with the modifier key <tt>C</tt>
(<tt>CONTROL</tt> on Linux or Windows,
<tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
windows by jEdit, which also allows multiple instances.</li>
<li>Prover process and source files are managed by the Scala layer on
the editor side. The prover experiences a mostly timeless and
stateless environment of formal document content.</li>
</ul>
<h2>Isabelle symbols and fonts</h2>
<ul>
<li>Isabelle supports infinitely many symbols:<br/>
α, β, γ, …<br/>
∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
≤, ≥, ⊓, ⊔, …<br/>
ℵ, △, ∇, …<br/>
<tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/>
</li>
<li>There are some special control symbols to modify the style of a
<em>single</em> symbol:<br/>
⇩ subscript<br/>
⇧ superscript<br/>
⇣ subscript within identifier<br/>
⇡ superscript within identifier<br/>
❙ bold face</li>
<li>A default mapping relates some Isabelle symbols to Unicode points
(see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
</li>
<li>The <em>IsabelleText</em> font ensures that Unicode points are actually
seen on the screen (or printer).
</li>
<li>Input methods:
<ul>
<li>copy/paste from decoded source files</li>
<li>copy/paste from prover output</li>
<li>completion provided by Isabelle plugin, e.g.<br/>
<table border="1">
<tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr>
<tr><td>lambda</td> <td><tt>%</tt></td> <td>λ</td></tr>
<tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr>
<tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr>
<tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr>
<tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr>
<tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr>
<tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr>
<tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr>
<tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr>
<tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr>
<tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr>
<tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr>
<tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr>
<tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr>
<tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr>
<tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr>
<tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr>
<tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr>
<tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr>
</table>
</li>
</ul>
</li>
<li><b>NOTE:</b> The above abbreviations refer to the input method.
The logical notation provides ASCII alternatives that often
coincide, but deviate occasionally.
</li>
<li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
source replacement operations; this works for Isabelle as long
as the Unicode sequences coincide with the symbol mapping.
</li>
<li><b>NOTE:</b> Raw unicode characters within prover source files
should be restricted to informal parts, e.g. to write text in
non-latin alphabets. Mathematical symbols should be defined via the
official rendering tables.
</li>
</ul>
<h2>Limitations and workrounds (October 2011)</h2>
<ul>
<li>No way to start/stop prover or switch to a different logic.<br/>
<em>Workaround:</em> Change options and restart editor.</li>
<li>Incremental reparsing sometimes produces unexpected command
spans.<br/>
<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
<li>Odd behavior of some diagnostic commands, notably those starting
external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
<em>Workaround:</em> Avoid such commands.</li>
<li>Lack of dependency managed for auxiliary files that contribute
to a theory ("<b>uses</b>").<br/>
<em>Workaround:</em> Re-use files manually within the prover.</li>
<li>Crude management of new Isar commands that are defined within
the running session.<br/>
<em>Workaround:</em> Force re-parsing of files using such commands
via reload menu of jEdit.</li>
<li>No way to delete document nodes from the overall collection of
theories.<br/>
<em>Workaround:</em> Restart whole Isabelle/jEdit session in
worst-case situation.</li>
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
loading external files.</li>
<li>General lack of various conveniences known from Proof
General.</li>
</ul>
<h2>Known problems with Mac OS X</h2>
<ul>
<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
e.g. between the editor and the Console plugin, which is a standard
swing text box. Similar for search boxes etc.</li>
<li><tt>Font.createFont</tt> mangles the font family of non-regular
fonts, e.g. bold. IsabelleText font files need to be
installed/updated manually if bold versions are desired. Note that
this has to be repeated whenever fonts shipped with Isabelle are
updated!</li>
<li>Missing glyphs are collected from other fonts (like Emacs,
Firefox). This is actually an advantage over the Oracle JVM on
Windows or Linux, but also the deeper reason for other oddities of
Apple font management.</li>
<li>The native font renderer
of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
enabled by default) fails to handle the infinitesimal font size of
"hidden" text (e.g. used in Isabelle sub/superscripts).</li>
</ul>
<h2>Known problems with OpenJDK 1.6.x</h2>
<ul>
<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
of the jEdit text area. Always use official JRE 1.6.x from Oracle
or Apple.</li>
<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
</ul>
<h2>Licenses and home sites of contributing systems</h2>
<ul>
<li>Isabelle: BSD-style</li>
<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
</ul>
</body>
</html>