# HG changeset patch
# User wenzelm
# Date 1350910358 -7200
# Node ID d9e08e2555f929159c7f4d9a9d5113eddd483d2e
# Parent  69774b4f5b8af9082f487d992bb6ef6d507c5709
more detailed Prover IDE NEWS;

diff -r 69774b4f5b8a -r d9e08e2555f9 NEWS
--- a/NEWS	Sun Oct 21 22:32:22 2012 +0200
+++ b/NEWS	Mon Oct 22 14:52:38 2012 +0200
@@ -6,17 +6,6 @@
 
 *** General ***
 
-* Prover IDE (PIDE) improvements:
-    . parallel terminal proofs ('by');
-    . improved output panel with tooltips, hyperlinks etc.;
-    . improved tooltips with nested tooltips, hyperlinks etc.;
-    . more efficient painting, improved reactivity;
-    . more robust incremental parsing of outer syntax (partial
-      comments, malformed symbols);
-    . smarter handling of tracing messages (via tracing_limit);
-    . more plugin options and preferences, based on Isabelle/Scala;
-    . uniform Java 7 platform on Linux, Mac OS X, Windows;
-
 * Configuration option show_markup controls direct inlining of markup
 into the printed representation of formal entities --- notably type
 and sort constraints.  This enables Prover IDE users to retrieve that
@@ -45,6 +34,46 @@
 lazy enumerations (method applications etc.).
 
 
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Parallel terminal proofs ('by') are enabled by default, likewise
+proofs that are built into packages like 'datatype', 'function'.  This
+allows to "run ahead" checking the theory specifications on the
+surface, while the prover is still crunching on internal
+justifications.  Unfinished / cancelled proofs are restarted as
+required to complete full proof checking eventually.
+
+* Improved output panel with tooltips, hyperlinks etc. based on the
+same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
+tooltips leads to some window that supports the same recursively,
+which can lead to stacks of tooltips as the semantic document content
+is explored.  ESCAPE closes the whole stack, individual windows may be
+closed separately, or detached to become independent jEdit dockables.
+
+* More robust incremental parsing of outer syntax (partial comments,
+malformed symbols).  Changing the balance of open/close quotes and
+comment delimiters works more conveniently with unfinished situations
+that frequently occur in user interaction.
+
+* More efficient painting and improved reactivity when editing large
+files.  More scalable management of formal document content.
+
+* Smarter handling of tracing messages: output window informs about
+accumulated messages; prover transactions are limited to emit maximum
+amount of output, before being canceled (cf. tracing_limit option).
+This avoids swamping the front-end with potentially infinite message
+streams.
+
+* More plugin options and preferences, based on Isabelle/Scala.  The
+jEdit plugin option panel provides access to some Isabelle/Scala
+options, including tuning parameters for editor reactivity and color
+schemes.
+
+* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
+from Oracle provide better multi-platform experience.  This version is
+now bundled exclusively with Isabelle.
+
+
 *** Pure ***
 
 * Code generation for Haskell: restrict unqualified imports from