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 |