<?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>Notes on the Isabelle/jEdit Prover IDE</title>
</head>
<body>
<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
The Isabelle/Scala layer that is already part of Isabelle/Pure
provides some general infrastructure for advanced prover interaction
and integration. The Isabelle/jEdit application serves as an example
for asynchronous proof checking with support for parallel processing.
<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>
</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>
</ul>
<h2>Limitations and workrounds (September 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>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>