From: Makarius <makarius@sketis.net>
* Isabelle/jEdit Prover IDE *
Action isabelle.select_structure (with keyboard shortcut C+7) extends
the editor selection by adding the enclosing formal structure, based on
formal markup by the prover. Repeated invocation of this action extends
the selection incrementally.
The Output dockable (and its variants used elsewhere) has been
improved as follows:
Its vertical scroll position is maintained more carefully, when
messages are printed incrementally.
Performance of printing messages repeatedly has improved slightly,
with less load on the GUI thread.
Highlighting works via mouse hovering alone, without requiring
C-modifier.
An active highlight area in the input buffer or output panel may be
turned into a text selection by using the ALT modifier.
This refers to Isabelle/7a7ad99212b1. I still need to update the documentation
(before the next release).
It might take some time until everybody realizes that we have a whole new life
concerning formal structure of inner syntax (in input and output).
Makarius
From: Makarius <makarius@sketis.net>
On 15/11/2024 23:41, Makarius wrote:
- The Output dockable (and its variants used elsewhere) has been
improved as follows:- Its vertical scroll position is maintained more carefully, when
messages are printed incrementally.- Performance of printing messages repeatedly has improved slightly,
with less load on the GUI thread.- Highlighting works via mouse hovering alone, without requiring
C-modifier.
- Search results are shown as tree view.
This refers to Isabelle/d421a7c58530.
It was surprisingly difficult to make the Java Swing JTree work properly: I've
imitated the regular HyperSearch results panel to some extent.
The JSplitPane is open by default, even without search results. I would prefer
to have it close, but the little triangles are only accesible to the user, not
via regular Java programming interfaces. (There are very ugly tricks to
imitate user clicks, but I did not try anything in that direction so far.)
Makarius
Last updated: Jan 05 2025 at 20:18 UTC