NEWS
changeset 49968 d9e08e2555f9
parent 49963 326f87427719
child 49972 f11f8905d9fd
equal deleted inserted replaced
49967:69774b4f5b8a 49968:d9e08e2555f9
     3 
     3 
     4 New in this Isabelle version
     4 New in this Isabelle version
     5 ----------------------------
     5 ----------------------------
     6 
     6 
     7 *** General ***
     7 *** General ***
     8 
       
     9 * Prover IDE (PIDE) improvements:
       
    10     . parallel terminal proofs ('by');
       
    11     . improved output panel with tooltips, hyperlinks etc.;
       
    12     . improved tooltips with nested tooltips, hyperlinks etc.;
       
    13     . more efficient painting, improved reactivity;
       
    14     . more robust incremental parsing of outer syntax (partial
       
    15       comments, malformed symbols);
       
    16     . smarter handling of tracing messages (via tracing_limit);
       
    17     . more plugin options and preferences, based on Isabelle/Scala;
       
    18     . uniform Java 7 platform on Linux, Mac OS X, Windows;
       
    19 
     8 
    20 * Configuration option show_markup controls direct inlining of markup
     9 * Configuration option show_markup controls direct inlining of markup
    21 into the printed representation of formal entities --- notably type
    10 into the printed representation of formal entities --- notably type
    22 and sort constraints.  This enables Prover IDE users to retrieve that
    11 and sort constraints.  This enables Prover IDE users to retrieve that
    23 information via tooltips in the output window, for example.
    12 information via tooltips in the output window, for example.
    41 specifications: nesting of "context fixes ... context assumes ..."
    30 specifications: nesting of "context fixes ... context assumes ..."
    42 and "class ... context ...".
    31 and "class ... context ...".
    43 
    32 
    44 * More informative error messages for Isar proof commands involving
    33 * More informative error messages for Isar proof commands involving
    45 lazy enumerations (method applications etc.).
    34 lazy enumerations (method applications etc.).
       
    35 
       
    36 
       
    37 *** Prover IDE -- Isabelle/Scala/jEdit ***
       
    38 
       
    39 * Parallel terminal proofs ('by') are enabled by default, likewise
       
    40 proofs that are built into packages like 'datatype', 'function'.  This
       
    41 allows to "run ahead" checking the theory specifications on the
       
    42 surface, while the prover is still crunching on internal
       
    43 justifications.  Unfinished / cancelled proofs are restarted as
       
    44 required to complete full proof checking eventually.
       
    45 
       
    46 * Improved output panel with tooltips, hyperlinks etc. based on the
       
    47 same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
       
    48 tooltips leads to some window that supports the same recursively,
       
    49 which can lead to stacks of tooltips as the semantic document content
       
    50 is explored.  ESCAPE closes the whole stack, individual windows may be
       
    51 closed separately, or detached to become independent jEdit dockables.
       
    52 
       
    53 * More robust incremental parsing of outer syntax (partial comments,
       
    54 malformed symbols).  Changing the balance of open/close quotes and
       
    55 comment delimiters works more conveniently with unfinished situations
       
    56 that frequently occur in user interaction.
       
    57 
       
    58 * More efficient painting and improved reactivity when editing large
       
    59 files.  More scalable management of formal document content.
       
    60 
       
    61 * Smarter handling of tracing messages: output window informs about
       
    62 accumulated messages; prover transactions are limited to emit maximum
       
    63 amount of output, before being canceled (cf. tracing_limit option).
       
    64 This avoids swamping the front-end with potentially infinite message
       
    65 streams.
       
    66 
       
    67 * More plugin options and preferences, based on Isabelle/Scala.  The
       
    68 jEdit plugin option panel provides access to some Isabelle/Scala
       
    69 options, including tuning parameters for editor reactivity and color
       
    70 schemes.
       
    71 
       
    72 * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
       
    73 from Oracle provide better multi-platform experience.  This version is
       
    74 now bundled exclusively with Isabelle.
    46 
    75 
    47 
    76 
    48 *** Pure ***
    77 *** Pure ***
    49 
    78 
    50 * Code generation for Haskell: restrict unqualified imports from
    79 * Code generation for Haskell: restrict unqualified imports from