equal
deleted
inserted
replaced
58 same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of |
58 same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of |
59 tooltips leads to some window that supports the same recursively, |
59 tooltips leads to some window that supports the same recursively, |
60 which can lead to stacks of tooltips as the semantic document content |
60 which can lead to stacks of tooltips as the semantic document content |
61 is explored. ESCAPE closes the whole stack, individual windows may be |
61 is explored. ESCAPE closes the whole stack, individual windows may be |
62 closed separately, or detached to become independent jEdit dockables. |
62 closed separately, or detached to become independent jEdit dockables. |
|
63 |
|
64 * Improved support for commands that produce graph output: the text |
|
65 message contains a clickable area to open a new instance of the graph |
|
66 browser on demand. |
63 |
67 |
64 * More robust incremental parsing of outer syntax (partial comments, |
68 * More robust incremental parsing of outer syntax (partial comments, |
65 malformed symbols). Changing the balance of open/close quotes and |
69 malformed symbols). Changing the balance of open/close quotes and |
66 comment delimiters works more conveniently with unfinished situations |
70 comment delimiters works more conveniently with unfinished situations |
67 that frequently occur in user interaction. |
71 that frequently occur in user interaction. |