src/Tools/jEdit/README.html
author wenzelm
Sun, 09 Oct 2011 16:47:58 +0200
changeset 45107 76fef3e57004
parent 45099 67740480cf39
child 46118 e99ca055c91d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
     1
<?xml version="1.0" encoding="UTF-8" ?>
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
     2
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
     3
<html xmlns="http://www.w3.org/1999/xhtml">
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
     4
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
     5
<head>
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
     6
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
43470
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
     7
<style type="text/css" media="screen">
43509
4414c8b02bf9 prefer STIXGeneral -- hard to tell if better or worse;
wenzelm
parents: 43472
diff changeset
     8
body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
43470
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
     9
</style>
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    10
<title>Welcome to the Isabelle/jEdit Prover IDE</title>
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    11
</head>
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    12
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    13
<body>
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    14
45099
67740480cf39 observe base URL of rendered document;
wenzelm
parents: 45098
diff changeset
    15
<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    16
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    17
<p>
45099
67740480cf39 observe base URL of rendered document;
wenzelm
parents: 45098
diff changeset
    18
  <b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    19
  based on Isabelle/Scala technology that is integrated with Isabelle.
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    20
  It is build around a concept of
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    21
  <em>asynchronous document processing</em>, which is supported
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    22
  natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    23
</p>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    24
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    25
<p>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    26
  <b>Isabelle/jEdit</b> is an example application within the PIDE
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    27
  framework &mdash; it illustrates many of the ideas in a realistic
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    28
  manner, ready to be used right now in Isabelle applications.
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    29
</p>
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
    30
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    31
<p>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    32
  <em>Research and implementation of concepts around PIDE has been
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    33
  kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    34
  Université Paris-Sud (http://www.u-psud.fr), and Digiteo
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    35
  (http://www.digiteo.fr).</em>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    36
</p>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    37
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    38
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    39
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    40
<h2>The Isabelle/jEdit Prover IDE</h2>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    41
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    42
<p>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    43
Isabelle/jEdit consists of some plugins for the well-known jEdit text
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    44
editor framework (http://www.jedit.org), according to the following
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    45
principles.
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    46
</p>
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    47
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    48
<ul>
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    49
39738
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    50
<li>The original jEdit look-and-feel is generally preserved, although
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    51
  some default properties have been changed to accommodate Isabelle
40894
a0f7ebe8f7a7 tuned README;
wenzelm
parents: 39815
diff changeset
    52
  (e.g. the text area font).</li>
39736
e19cece7d18a tuned README;
wenzelm
parents: 39591
diff changeset
    53
39738
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    54
<li>Formal Isabelle/Isar text is checked asynchronously while editing.
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    55
  The user is in full command of the editor, and the prover refrains
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    56
  from locking portions of the buffer etc.</li>
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    57
39738
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    58
<li>Prover feedback works via tooltips, syntax highlighting, colors,
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    59
  boxes etc. based on semantic markup provided by Isabelle in the
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    60
  background.</li>
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    61
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    62
<li>Using the mouse together with the modifier key <tt>C</tt>
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    63
(<tt>CONTROL</tt> on Linux or Windows,
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
    64
  <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
39736
e19cece7d18a tuned README;
wenzelm
parents: 39591
diff changeset
    65
39738
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    66
<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
909ee37c34c1 tuned README;
wenzelm
parents: 39736
diff changeset
    67
  windows by jEdit, which also allows multiple instances.</li>
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    68
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    69
<li>Prover process and source files are managed by the Scala layer on
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    70
the editor side.  The prover experiences a mostly timeless and
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    71
stateless environment of formal document content.</li>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
    72
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    73
</ul>
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
    74
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    75
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    76
<h2>Isabelle symbols and fonts</h2>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    77
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    78
<ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    79
  <li>Isabelle supports infinitely many symbols:<br/>
43472
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    80
    α, β, γ, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    81
    ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    82
    ≤, ≥, ⊓, ⊔, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    83
    ℵ, △, ∇, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    84
    <tt>\&lt;foo&gt;</tt>, <tt>\&lt;bar&gt;</tt>, <tt>\&lt;baz&gt;</tt>, …<br/>
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    85
  </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    86
43470
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
    87
  <li>There are some special control symbols to modify the style of a
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
    88
  <em>single</em> symbol:<br/>
43472
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    89
    ⇩ subscript<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    90
    ⇧ superscript<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    91
    ⇣ subscript within identifier<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    92
    ⇡ superscript within identifier<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
    93
    ❙ bold face</li>
43470
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
    94
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    95
  <li>A default mapping relates some Isabelle symbols to Unicode points
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    96
    (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    97
  </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    98
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
    99
  <li>The <em>IsabelleText</em> font ensures that Unicode points are actually
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   100
    seen on the screen (or printer).
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   101
  </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   102
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   103
  <li>Input methods:
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   104
    <ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   105
      <li>copy/paste from decoded source files</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   106
      <li>copy/paste from prover output</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   107
      <li>completion provided by Isabelle plugin, e.g.<br/>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   108
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   109
      <table border="1">
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   110
      <tr><th><b>name</b></th>    <th><b>abbreviation</b></th>  <th><b>symbol</b></th></tr>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   111
43472
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   112
      <tr><td>lambda</td>         <td><tt>%</tt></td>           <td>λ</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   113
      <tr><td>Rightarrow</td>     <td><tt>=&gt;</tt></td>       <td>⇒</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   114
      <tr><td>Longrightarrow</td> <td><tt>==&gt;</tt></td>      <td>⟹</td></tr>
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   115
43472
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   116
      <tr><td>And</td>            <td><tt>!!</tt></td>          <td>⋀</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   117
      <tr><td>equiv</td>          <td><tt>==</tt></td>          <td>≡</td></tr>
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   118
43472
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   119
      <tr><td>forall</td>         <td><tt>!</tt></td>           <td>∀</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   120
      <tr><td>exists</td>         <td><tt>?</tt></td>           <td>∃</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   121
      <tr><td>longrightarrow</td> <td><tt>--&gt;</tt></td>      <td>⟶</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   122
      <tr><td>and</td>            <td><tt>/\</tt></td>          <td>∧</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   123
      <tr><td>or</td>             <td><tt>\/</tt></td>          <td>∨</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   124
      <tr><td>not</td>            <td><tt>~ </tt></td>          <td>¬</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   125
      <tr><td>noteq</td>          <td><tt>~=</tt></td>          <td>≠</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   126
      <tr><td>in</td>             <td><tt>:</tt></td>           <td>∈</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   127
      <tr><td>notin</td>          <td><tt>~:</tt></td>          <td>∉</td></tr>
43470
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
   128
43472
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   129
      <tr><td>sub</td>            <td><tt>=_</tt></td>          <td>⇩</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   130
      <tr><td>sup</td>            <td><tt>=^</tt></td>          <td>⇧</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   131
      <tr><td>isup</td>           <td><tt>-_</tt></td>          <td>⇣</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   132
      <tr><td>isub</td>           <td><tt>-^</tt></td>          <td>⇡</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output;
wenzelm
parents: 43470
diff changeset
   133
      <tr><td>bold</td>           <td><tt>-.</tt></td>          <td>❙</td></tr>
43470
3d42dea16357 explain special control symbols;
wenzelm
parents: 43287
diff changeset
   134
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   135
    </table>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   136
    </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   137
  </ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   138
  </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   139
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   140
  <li><b>NOTE:</b> The above abbreviations refer to the input method.
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   141
    The logical notation provides ASCII alternatives that often
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   142
    coincide, but deviate occasionally.
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   143
  </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   144
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   145
  <li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   146
    source replacement operations; this works for Isabelle as long
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   147
    as the Unicode sequences coincide with the symbol mapping.
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   148
  </li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   149
45107
wenzelm
parents: 45099
diff changeset
   150
  <li><b>NOTE:</b> Raw unicode characters within prover source files
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   151
  should be restricted to informal parts, e.g. to write text in
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   152
  non-latin alphabets.  Mathematical symbols should be defined via the
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   153
  official rendering tables.
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   154
  </li>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   155
41628
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   156
</ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   157
ed4d793f0c26 improved README -- Isabelle symbols and fonts;
wenzelm
parents: 41538
diff changeset
   158
45107
wenzelm
parents: 45099
diff changeset
   159
<h2>Limitations and workrounds (October 2011)</h2>
41538
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   160
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   161
<ul>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   162
  <li>No way to start/stop prover or switch to a different logic.<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   163
  <em>Workaround:</em> Change options and restart editor.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   164
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   165
  <li>Incremental reparsing sometimes produces unexpected command
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   166
  spans.<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   167
  <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   168
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   169
  <li>Odd behavior of some diagnostic commands, notably those starting
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   170
  external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   171
  <em>Workaround:</em> Avoid such commands.</li>
41538
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   172
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   173
  <li>Lack of dependency managed for auxiliary files that contribute
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   174
  to a theory ("<b>uses</b>").<br/>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   175
  <em>Workaround:</em> Re-use files manually within the prover.</li>
41538
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   176
44759
9572b6be1aab more README;
wenzelm
parents: 44700
diff changeset
   177
  <li>Crude management of new Isar commands that are defined within
9572b6be1aab more README;
wenzelm
parents: 44700
diff changeset
   178
  the running session.<br/>
9572b6be1aab more README;
wenzelm
parents: 44700
diff changeset
   179
  <em>Workaround:</em> Force re-parsing of files using such commands
9572b6be1aab more README;
wenzelm
parents: 44700
diff changeset
   180
  via reload menu of jEdit.</li>
9572b6be1aab more README;
wenzelm
parents: 44700
diff changeset
   181
44806
3950842bb628 more README;
wenzelm
parents: 44759
diff changeset
   182
  <li>No way to delete document nodes from the overall collection of
3950842bb628 more README;
wenzelm
parents: 44759
diff changeset
   183
  theories.<br/>
3950842bb628 more README;
wenzelm
parents: 44759
diff changeset
   184
  <em>Workaround:</em> Restart whole Isabelle/jEdit session in
3950842bb628 more README;
wenzelm
parents: 44759
diff changeset
   185
  worst-case situation.</li>
3950842bb628 more README;
wenzelm
parents: 44759
diff changeset
   186
41538
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   187
  <li>No support for non-local markup, e.g. commands reporting on
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   188
  previous commands (proof end on proof head), or markup produced by
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   189
  loading external files.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   190
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   191
  <li>General lack of various conveniences known from Proof
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   192
  General.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   193
</ul>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds;
wenzelm
parents: 40894
diff changeset
   194
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   195
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   196
<h2>Known problems with Mac OS X</h2>
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   197
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   198
<ul>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   199
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   200
<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   201
  e.g. between the editor and the Console plugin, which is a standard
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   202
  swing text box.  Similar for search boxes etc.</li>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   203
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   204
<li><tt>Font.createFont</tt> mangles the font family of non-regular
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   205
  fonts, e.g. bold.  IsabelleText font files need to be
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   206
  installed/updated manually if bold versions are desired.  Note that
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   207
  this has to be repeated whenever fonts shipped with Isabelle are
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   208
  updated!</li>
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   209
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   210
<li>Missing glyphs are collected from other fonts (like Emacs,
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   211
  Firefox).  This is actually an advantage over the Oracle JVM on
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   212
  Windows or Linux, but also the deeper reason for other oddities of
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   213
  Apple font management.</li>
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   214
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   215
<li>The native font renderer
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   216
  of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   217
  enabled by default) fails to handle the infinitesimal font size of
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   218
  "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   219
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   220
</ul>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   221
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   222
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   223
<h2>Known problems with OpenJDK 1.6.x</h2>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   224
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   225
<ul>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   226
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   227
<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   228
  of the jEdit text area.  Always use official JRE 1.6.x from Oracle
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   229
  or Apple.</li>
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   230
45097
d0f851903e55 tuned README.html;
wenzelm
parents: 44875
diff changeset
   231
<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
44875
68615b48cc12 more README;
wenzelm
parents: 44806
diff changeset
   232
68615b48cc12 more README;
wenzelm
parents: 44806
diff changeset
   233
</ul>
68615b48cc12 more README;
wenzelm
parents: 44806
diff changeset
   234
68615b48cc12 more README;
wenzelm
parents: 44806
diff changeset
   235
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   236
<h2>Licenses and home sites of contributing systems</h2>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   237
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   238
<ul>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   239
45098
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   240
<li>Isabelle: BSD-style</li>
37c89c5cc601 more README;
wenzelm
parents: 45097
diff changeset
   241
44700
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   242
<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   243
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   244
<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   245
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   246
<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   247
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   248
</ul>
f4b42f310f86 updated READMEs;
wenzelm
parents: 44203
diff changeset
   249
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
   250
</body>
a43a723753e6 more content for Session_Dockable;
wenzelm
parents:
diff changeset
   251
</html>