equal
deleted
inserted
replaced
88 situations. The text overview column takes over the role to indicate |
88 situations. The text overview column takes over the role to indicate |
89 unfinished edits in the PIDE pipeline. This avoids flashing text display |
89 unfinished edits in the PIDE pipeline. This avoids flashing text display |
90 due to ad-hoc updates by auxiliary GUI components, such as the State |
90 due to ad-hoc updates by auxiliary GUI components, such as the State |
91 panel. |
91 panel. |
92 |
92 |
93 * Improved scheduling for urgent print tasks (e.g. command state output, |
93 * Slightly improved scheduling for urgent print tasks (e.g. command |
94 interactive queries) wrt. long-running background tasks. |
94 state output, interactive queries) wrt. long-running background tasks. |
95 |
95 |
96 * Completion of symbols via prefix of \<name> or \<^name> or \name is |
96 * Completion of symbols via prefix of \<name> or \<^name> or \name is |
97 always possible, independently of the language context. It is never |
97 always possible, independently of the language context. It is never |
98 implicit: a popup will show up unconditionally. |
98 implicit: a popup will show up unconditionally. |
99 |
99 |