author wenzelm
Sat, 25 May 2013 17:40:44 +0200
changeset 52147 9943f8067f11
parent 51621 8c0f6caba80e
child 53021 d0fa3f446b9d
permissions -rw-r--r--

<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "">
<html xmlns="">

<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<style type="text/css" media="screen">
body { font-family: IsabelleText; font-size: 14pt; }
<title>Welcome to the Isabelle/jEdit Prover IDE</title>


<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>

  <b>PIDE</b> is a framework for Prover IDEs based on the
  Isabelle/Scala.  It is built around a concept of
  <em>asynchronous document processing</em>, which is supported
  natively by the <em>parallel proof engine</em> that is implemented
  in Isabelle/ML.

  <b>Isabelle/jEdit</b> is the main example application of the PIDE
  framework &mdash; it is ready for small and large Isabelle
  applications, for beginners and experts alike.

  <em>Research and implementation of concepts around PIDE has started
  around 2008 and was kindly supported by BMBF (,
  Université Paris-Sud (, Digiteo
  (, and ANR

<h2>The Isabelle/jEdit Prover IDE</h2>

Isabelle/jEdit consists of some plugins for the well-known jEdit text
editor framework (, according to the following


<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.</li>

<li>Prover feedback works via colors, boxes, squiggly underline,
hyperlinks, popup windows, icons, clickable output, all based on semantic
markup produced by Isabelle in the background.</li>

<li>Using the mouse together with the modifier key <tt>CONTROL</tt> (Linux,
Windows) or <tt>COMMAND</tt> (Mac OS X) exposes additional formal

<li>Dockable panels (e.g. <em>Output</em>, <em>Symbols</em>) are managed as
independent windows by jEdit, which also allows multiple instances.</li>

<li>Formal output (in popups etc.) may be explored recursively, using the
same techniques as in the editor source buffer.</li>

<li>The prover process and source files are managed on the editor side. The
prover operates on timeless and stateless document content via

<li>Plugin options of jEdit (for the <em>Isabelle</em> plugin) give access
to a selection of Isabelle/Scala options and its persistence preferences,
usually with immediate effect on the prover back-end or editor

<li>The logic image of the prover session may be specified within
Isabelle/jEdit, but this requires restart. The new image is provided
automatically by the Isabelle build process.</li>


<h2>Isabelle symbols and fonts</h2>

  <li>Isabelle supports infinitely many symbols:<br/>
    α, β, γ, …<br/>
    ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
    ≤, ≥, ⊓, ⊔, …<br/>
    ℵ, △, ∇, …<br/>
    <tt>\&lt;foo&gt;</tt>, <tt>\&lt;bar&gt;</tt>, <tt>\&lt;baz&gt;</tt>, …<br/>

  <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>The <em>IsabelleText</em> font ensures that Unicode points are actually
    seen on the screen (or printer).

  <li>Input methods:
      <li>use the Symbols dockable</li>
      <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>=&gt;</tt></td>       <td>⇒</td></tr>
      <tr><td>Longrightarrow</td> <td><tt>==&gt;</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>--&gt;</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>


  <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><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><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><b>NOTE:</b> Control symbols may be applied to a region of selected
    text, either using the Symbols dockable or keyboard shortcuts.</li>


<h2>Limitations and known problems</h2>

  <li>Keyboard shortcuts C-PLUS and C-MINUS for adjusting the editor font
  size depend on platform details and national keyboards.<br/>
  <em>Workaround: Use numeric keypad or rebind keys in the jEdit Shortcuts
  options dialog.</em></li>

  <li>Lack of dependency management for auxiliary files that contribute
  to a theory (e.g. <tt>ML_file</tt>).<br/>
  <em>Workaround:</em> Re-load files manually within the prover.</li>

  <li>Odd behavior of some diagnostic commands with global
  side-effects, like writing a physical
  <em>Workaround:</em> Avoid such commands.</li>

  <li>No way to delete document nodes from the overall collection of
  <em>Workaround:</em> Restart whole Isabelle/jEdit session in
  worst-case situation.</li>

  <li>Linux: some desktop environments with extreme animation effects
  may disrupt Java 7 window placement and keyboard focus.<br/>
  <em>Workaround:</em> Disable such effects.</li>

  <li>Linux: some X11 window managers that are not "re-parenting"
  cause problems with additional windows opened by the Java VM. This
  affects either historic or neo-minimalistic window managers like
  <em>awesome</em> or <em>xmonad</em>.<br/>
  <em>Workaround:</em> Use regular re-parenting window manager.</li>

  <li>Mac OS X: the native MacOSX plugin for jEdit tends to be
  disruptive and is off by default. Enabling it might or might not
  improve the user experience.<br/>
  <em>Workaround:</em> Disable MacOSX plugin.</li></li>

  <li>Mac OS X: Java 7 is officially supported on Lion and Mountain Lion,
  but not Snow Leopard. It usually works on the latter, although with a
  small risk of instabilities.<br/>
  <em>Workaround:</em> Update to OS X Mountain Lion.</li>

<h2>Licenses and home sites of contributing systems</h2>


<li>Isabelle: BSD-style</li>

<li>Poly/ML: LGPL <br/> </li>

<li>Scala: BSD-style <br/></li>

<li>jEdit: GPL (with special cases) <br/></li>

<li>JFreeChart: LGPL <br/></li>

<li>Lobo/Cobra: GPL and LGPL <br/></li>