--- a/src/Tools/jEdit/dist-template/README.html Wed Jun 08 17:01:07 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-<?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"/>
-<title>Notes on the Isabelle/jEdit Prover IDE</title>
-</head>
-
-<body>
-
-<h2>The Isabelle/jEdit Prover IDE</h2>
-
-<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>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></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>
- </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 (January 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>Multiple theory buffers cannot depend on each other, imports are
- resolved via the file-system.<br/>
- <em>Workaround:</em> Save/reload files manually.</li>
-
- <li>No reclaiming of old/unused document versions in prover or
- editor.<br/>
- <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
-
- <li>Incremental reparsing sometimes produces unexpected command
- spans.<br/>
- <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
-
- <li>Command execution sometimes gets stuck (purple background).<br/>
- <em>Workaround:</em> Force reparsing as above.</li>
-
- <li>Odd behavior of some diagnostic commands, notably those
- starting external processes asynchronously
- (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
- <em>Workaround:</em> Avoid such commands.</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>
-
-</body>
-</html>
-