<commit_before><?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>Welcome to the Isabelle/jEdit Prover IDE</title>
</head>

<body>

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

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

<p>
  <b>Isabelle/jEdit</b> is an example application within the PIDE
  framework &mdash; it illustrates many of the ideas in a realistic
  manner, ready to be used right now in Isabelle applications.
</p>

<p>
  <em>Research and implementation of concepts around PIDE has been
  kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
  Université Paris-Sud (http://www.u-psud.fr), and Digiteo
  (http://www.digiteo.fr).</em>
</p>



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

<p>
Isabelle/jEdit consists of some plugins for the well-known jEdit text
editor framework (http://www.jedit.org), according to the following
principles.
</p>

<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 X) 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>

<li>Prover process and source files are managed by the Scala layer on
the editor side.  The prover experiences a mostly timeless and
stateless environment of formal document content.</li>

</ul>


<h2>Isabelle symbols and fonts</h2>

<ul>
  <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>

  <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>=&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>

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

  <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>

</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 X</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><tt>Font.createFont</tt> mangles the font family of non-regular
  fonts, e.g. bold.  IsabelleText font files need to be
  installed/updated manually if bold versions are desired.  Note that
  this has to be repeated whenever fonts shipped with Isabelle are
  updated!</li>

<li>Missing glyphs are collected from other fonts (like Emacs,
  Firefox).  This is actually an advantage over the Oracle JVM on
  Windows or Linux, but also the deeper reason for other oddities of
  Apple font management.</li>

<li>The native font renderer
  of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
  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 Oracle
  or Apple.</li>

<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>

</ul>


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

<ul>

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

<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>
<commit_msg>tuned;<commit_after><?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>Welcome to the Isabelle/jEdit Prover IDE</title>
</head>

<body>

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

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

<p>
  <b>Isabelle/jEdit</b> is an example application within the PIDE
  framework &mdash; it illustrates many of the ideas in a realistic
  manner, ready to be used right now in Isabelle applications.
</p>

<p>
  <em>Research and implementation of concepts around PIDE has been
  kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
  Université Paris-Sud (http://www.u-psud.fr), and Digiteo
  (http://www.digiteo.fr).</em>
</p>



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

<p>
Isabelle/jEdit consists of some plugins for the well-known jEdit text
editor framework (http://www.jedit.org), according to the following
principles.
</p>

<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 X) 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>

<li>Prover process and source files are managed by the Scala layer on
the editor side.  The prover experiences a mostly timeless and
stateless environment of formal document content.</li>

</ul>


<h2>Isabelle symbols and fonts</h2>

<ul>
  <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>

  <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>=&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>

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

  <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>

</ul>


<h2>Limitations and workrounds (October 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 X</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><tt>Font.createFont</tt> mangles the font family of non-regular
  fonts, e.g. bold.  IsabelleText font files need to be
  installed/updated manually if bold versions are desired.  Note that
  this has to be repeated whenever fonts shipped with Isabelle are
  updated!</li>

<li>Missing glyphs are collected from other fonts (like Emacs,
  Firefox).  This is actually an advantage over the Oracle JVM on
  Windows or Linux, but also the deeper reason for other oddities of
  Apple font management.</li>

<li>The native font renderer
  of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
  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 Oracle
  or Apple.</li>

<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>

</ul>


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

<ul>

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

<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>

{'fraction_non_alphanumeric': 0.1665531721711497, 'fraction_numerical': 0.005561230280331404, 'mean_word_length': 3.174088109900521, 'pattern_counts': {'":': 0, '<': 821, '<?xml version=': 2, '>': 821, 'https://': 0, 'lorem ipsum': 0, 'www.': 16, 'xml': 4}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1753435', 'n_tokens_mistral': 6410, 'n_tokens_neox': 6105, 'n_words': 1843}