more detailed Prover IDE NEWS;
authorwenzelm
Mon Oct 22 14:52:38 2012 +0200 (2012-10-22)
changeset 49968d9e08e2555f9
parent 49967 69774b4f5b8a
child 49969 72216713733a
more detailed Prover IDE NEWS;
NEWS
     1.1 --- a/NEWS	Sun Oct 21 22:32:22 2012 +0200
     1.2 +++ b/NEWS	Mon Oct 22 14:52:38 2012 +0200
     1.3 @@ -6,17 +6,6 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Prover IDE (PIDE) improvements:
     1.8 -    . parallel terminal proofs ('by');
     1.9 -    . improved output panel with tooltips, hyperlinks etc.;
    1.10 -    . improved tooltips with nested tooltips, hyperlinks etc.;
    1.11 -    . more efficient painting, improved reactivity;
    1.12 -    . more robust incremental parsing of outer syntax (partial
    1.13 -      comments, malformed symbols);
    1.14 -    . smarter handling of tracing messages (via tracing_limit);
    1.15 -    . more plugin options and preferences, based on Isabelle/Scala;
    1.16 -    . uniform Java 7 platform on Linux, Mac OS X, Windows;
    1.17 -
    1.18  * Configuration option show_markup controls direct inlining of markup
    1.19  into the printed representation of formal entities --- notably type
    1.20  and sort constraints.  This enables Prover IDE users to retrieve that
    1.21 @@ -45,6 +34,46 @@
    1.22  lazy enumerations (method applications etc.).
    1.23  
    1.24  
    1.25 +*** Prover IDE -- Isabelle/Scala/jEdit ***
    1.26 +
    1.27 +* Parallel terminal proofs ('by') are enabled by default, likewise
    1.28 +proofs that are built into packages like 'datatype', 'function'.  This
    1.29 +allows to "run ahead" checking the theory specifications on the
    1.30 +surface, while the prover is still crunching on internal
    1.31 +justifications.  Unfinished / cancelled proofs are restarted as
    1.32 +required to complete full proof checking eventually.
    1.33 +
    1.34 +* Improved output panel with tooltips, hyperlinks etc. based on the
    1.35 +same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
    1.36 +tooltips leads to some window that supports the same recursively,
    1.37 +which can lead to stacks of tooltips as the semantic document content
    1.38 +is explored.  ESCAPE closes the whole stack, individual windows may be
    1.39 +closed separately, or detached to become independent jEdit dockables.
    1.40 +
    1.41 +* More robust incremental parsing of outer syntax (partial comments,
    1.42 +malformed symbols).  Changing the balance of open/close quotes and
    1.43 +comment delimiters works more conveniently with unfinished situations
    1.44 +that frequently occur in user interaction.
    1.45 +
    1.46 +* More efficient painting and improved reactivity when editing large
    1.47 +files.  More scalable management of formal document content.
    1.48 +
    1.49 +* Smarter handling of tracing messages: output window informs about
    1.50 +accumulated messages; prover transactions are limited to emit maximum
    1.51 +amount of output, before being canceled (cf. tracing_limit option).
    1.52 +This avoids swamping the front-end with potentially infinite message
    1.53 +streams.
    1.54 +
    1.55 +* More plugin options and preferences, based on Isabelle/Scala.  The
    1.56 +jEdit plugin option panel provides access to some Isabelle/Scala
    1.57 +options, including tuning parameters for editor reactivity and color
    1.58 +schemes.
    1.59 +
    1.60 +* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
    1.61 +from Oracle provide better multi-platform experience.  This version is
    1.62 +now bundled exclusively with Isabelle.
    1.63 +
    1.64 +
    1.65  *** Pure ***
    1.66  
    1.67  * Code generation for Haskell: restrict unqualified imports from