more README;
authorwenzelm
Tue Sep 27 21:39:55 2011 +0200 (2011-09-27 ago)
changeset 4509837c89c5cc601
parent 45097 d0f851903e55
child 45099 67740480cf39
more README;
src/Tools/jEdit/README.html
     1.1 --- a/src/Tools/jEdit/README.html	Tue Sep 27 20:45:15 2011 +0200
     1.2 +++ b/src/Tools/jEdit/README.html	Tue Sep 27 21:39:55 2011 +0200
     1.3 @@ -7,17 +7,43 @@
     1.4  <style type="text/css" media="screen">
     1.5  body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
     1.6  </style>
     1.7 -<title>Notes on the Isabelle/jEdit Prover IDE</title>
     1.8 +<title>Welcome to the Isabelle/jEdit Prover IDE</title>
     1.9  </head>
    1.10  
    1.11  <body>
    1.12  
    1.13 -<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
    1.14 +<h2>The PIDE framework</h2>
    1.15 +
    1.16 +<p>
    1.17 +  <b>PIDE</b> is an emerging framework for sophisticated Prover IDEs,
    1.18 +  based on Isabelle/Scala technology that is integrated with Isabelle.
    1.19 +  It is build around a concept of
    1.20 +  <em>asynchronous document processing</em>, which is supported
    1.21 +  natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
    1.22 +</p>
    1.23 +
    1.24 +<p>
    1.25 +  <b>Isabelle/jEdit</b> is an example application within the PIDE
    1.26 +  framework &mdash; it illustrates many of the ideas in a realistic
    1.27 +  manner, ready to be used right now in Isabelle applications.
    1.28 +</p>
    1.29  
    1.30 -The Isabelle/Scala layer that is already part of Isabelle/Pure
    1.31 -provides some general infrastructure for advanced prover interaction
    1.32 -and integration.  The Isabelle/jEdit application serves as an example
    1.33 -for asynchronous proof checking with support for parallel processing.
    1.34 +<p>
    1.35 +  <em>Research and implementation of concepts around PIDE has been
    1.36 +  kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
    1.37 +  Université Paris-Sud (http://www.u-psud.fr), and Digiteo
    1.38 +  (http://www.digiteo.fr).</em>
    1.39 +</p>
    1.40 +
    1.41 +
    1.42 +
    1.43 +<h2>The Isabelle/jEdit Prover IDE</h2>
    1.44 +
    1.45 +<p>
    1.46 +Isabelle/jEdit consists of some plugins for the well-known jEdit text
    1.47 +editor framework (http://www.jedit.org), according to the following
    1.48 +principles.
    1.49 +</p>
    1.50  
    1.51  <ul>
    1.52  
    1.53 @@ -40,13 +66,16 @@
    1.54  <li>Dockable panels (e.g. <em>Output</em>) are managed as independent
    1.55    windows by jEdit, which also allows multiple instances.</li>
    1.56  
    1.57 +<li>Prover process and source files are managed by the Scala layer on
    1.58 +the editor side.  The prover experiences a mostly timeless and
    1.59 +stateless environment of formal document content.</li>
    1.60 +
    1.61  </ul>
    1.62  
    1.63  
    1.64  <h2>Isabelle symbols and fonts</h2>
    1.65  
    1.66  <ul>
    1.67 -
    1.68    <li>Isabelle supports infinitely many symbols:<br/>
    1.69      α, β, γ, …<br/>
    1.70      ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
    1.71 @@ -118,6 +147,12 @@
    1.72      as the Unicode sequences coincide with the symbol mapping.
    1.73    </li>
    1.74  
    1.75 +  <li><b>NOTE:</b>Raw unicode characters within prover source files
    1.76 +  should be restricted to informal parts, e.g. to write text in
    1.77 +  non-latin alphabets.  Mathematical symbols should be defined via the
    1.78 +  official rendering tables.
    1.79 +  </li>
    1.80 +
    1.81  </ul>
    1.82  
    1.83  
    1.84 @@ -202,6 +237,8 @@
    1.85  
    1.86  <ul>
    1.87  
    1.88 +<li>Isabelle: BSD-style</li>
    1.89 +
    1.90  <li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
    1.91  
    1.92  <li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>