88 |
88 |
89 * Action isabelle.reset-font-size resets main text area font size |
89 * Action isabelle.reset-font-size resets main text area font size |
90 according to Isabelle/Scala plugin option "jedit_font_reset_size" |
90 according to Isabelle/Scala plugin option "jedit_font_reset_size" |
91 (cf. keyboard shortcut C+0). |
91 (cf. keyboard shortcut C+0). |
92 |
92 |
93 * More reactive and less intrusive completion, managed by |
|
94 Isabelle/jEdit instead of SideKick. Plain words need to be at least 3 |
|
95 characters long to be completed (was 2 before). Symbols are only |
|
96 completed in backslash forms, e.g. \forall or \<forall> that both |
|
97 produce the Isabelle symbol \<forall> in its Unicode rendering. |
|
98 |
|
99 * Standard jEdit completion via C+b uses action isabelle.complete |
|
100 with fall-back on complete-word for non-Isabelle buffers. |
|
101 |
|
102 * Improved support for Linux look-and-feel "GTK+", see also "Utilities |
93 * Improved support for Linux look-and-feel "GTK+", see also "Utilities |
103 / Global Options / Appearance". |
94 / Global Options / Appearance". |
|
95 |
|
96 * Improved completion mechanism, which is now managed by the |
|
97 Isabelle/jEdit plugin instead of SideKick. |
|
98 |
|
99 - Various Isabelle plugin options to control popup behaviour and |
|
100 immediate insertion into buffer. |
|
101 |
|
102 - Light-weight popup, which avoids explicit window (more reactive |
|
103 and more robust). Interpreted key events: TAB, ESCAPE, UP, DOWN, |
|
104 PAGE_UP, PAGE_DOWN. All other key events are passed to the jEdit |
|
105 text area unchanged. |
|
106 |
|
107 - Explicit completion via standard jEdit shortcut C+b, which has |
|
108 been remapped to action "isabelle.complete" (fall-back on regular |
|
109 "complete-word" for non-Isabelle buffers). |
|
110 |
|
111 - Implicit completion via keyboard input on text area, with popup or |
|
112 immediate insertion into buffer. |
|
113 |
|
114 - Implicit completion of plain words requires at least 3 characters |
|
115 (was 2 before). |
|
116 |
|
117 - Immediate completion ignores plain words; it requires > 1 |
|
118 characters of symbol abbreviation to complete, otherwise fall-back |
|
119 on completion popup. |
|
120 |
|
121 - Isabelle Symbols are only completed in backslashed forms, |
|
122 e.g. \forall or \<forall> that both produce the Isabelle symbol |
|
123 \<forall> in its Unicode rendering. |
|
124 |
|
125 - Refined table of Isabelle symbol abbreviations (see |
|
126 $ISABELLE_HOME/etc/symbols). |
104 |
127 |
105 |
128 |
106 *** Pure *** |
129 *** Pure *** |
107 |
130 |
108 * Type theory is now immutable, without any special treatment of |
131 * Type theory is now immutable, without any special treatment of |