src/Tools/jEdit/dist-template/README.html
author wenzelm
Thu, 13 Jan 2011 18:00:13 +0100
changeset 41538 d060ccad02bd
parent 40894 a0f7ebe8f7a7
child 41628 ed4d793f0c26
permissions -rw-r--r--
updated Isabelle/jEdit limitations and workarounds;

<?xml version="1.0" encoding="ISO-8859-1" ?>
<!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>Notes on 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>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>