# HG changeset patch
# User wenzelm
# Date 1317152395 -7200
# Node ID 37c89c5cc6012099053ce0a16bd6087d1f28842e
# Parent d0f851903e55e859f6063b598f94929e166f562b
more README;
diff -r d0f851903e55 -r 37c89c5cc601 src/Tools/jEdit/README.html
--- a/src/Tools/jEdit/README.html Tue Sep 27 20:45:15 2011 +0200
+++ b/src/Tools/jEdit/README.html Tue Sep 27 21:39:55 2011 +0200
@@ -7,17 +7,43 @@
-Notes on the Isabelle/jEdit Prover IDE
+Welcome to the Isabelle/jEdit Prover IDE
-The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)
+The PIDE framework
+
+
+ PIDE is an emerging framework for sophisticated Prover IDEs,
+ based on Isabelle/Scala technology that is integrated with Isabelle.
+ It is build around a concept of
+ asynchronous document processing, which is supported
+ natively by the parallel proof engine implemented in Isabelle/ML.
+
+
+
+ Isabelle/jEdit is an example application within the PIDE
+ framework — it illustrates many of the ideas in a realistic
+ manner, ready to be used right now in Isabelle applications.
+
-The Isabelle/Scala layer that is already part of Isabelle/Pure
-provides some general infrastructure for advanced prover interaction
-and integration. The Isabelle/jEdit application serves as an example
-for asynchronous proof checking with support for parallel processing.
+
+ 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).
+
+
+
+
+The Isabelle/jEdit Prover IDE
+
+
+Isabelle/jEdit consists of some plugins for the well-known jEdit text
+editor framework (http://www.jedit.org), according to the following
+principles.
+
@@ -40,13 +66,16 @@
- Dockable panels (e.g. Output) are managed as independent
windows by jEdit, which also allows multiple instances.
+- 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.
+
Isabelle symbols and fonts
-
- Isabelle supports infinitely many symbols:
α, β, γ, …
∀, ∃, ∨, ∧, ⟶, ⟷, …
@@ -118,6 +147,12 @@
as the Unicode sequences coincide with the symbol mapping.
+ - NOTE: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.
+
+
@@ -202,6 +237,8 @@
+- Isabelle: BSD-style
+
- Scala: BSD-style
http://www.scala-lang.org
- jEdit: GPL (with special cases)
http://www.jedit.org/