<?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) 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</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>ToggleButton selected state is not rendered if window focus is
lost, which is probably a genuine feature of the Apple
look-and-feel.</li>
<li>Font.createFont mangles the font family of non-regular fonts,
e.g. bold. IsabelleText font files need to be installed/updated
manually.</li>
<li>Missing glyphs are collected from other fonts (like Emacs,
Firefox). This is actually an advantage over the Oracle/Sun JVM on
Windows or Linux, but probably also the deeper reason for the other
oddities of Apple font management.</li>
<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
(not 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
Sun/Oracle/Apple.</li>
<li>jEdit on OpenJDK is generally not supported.</li>
</ul>
<h2>Known problems with Windows/Cygwin</h2>
<ul>
<li>Occasional session startup problems when loading a logic image
takes too long (cf. output in "Prover Session / Syslog" panel).</li>
<li>Auxiliary files of a theory (<tt>uses</tt>) cannot be loaded due
to incompatible path notation inherited from MS-DOS.</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>