Email Gateway (Feb 06 2025 at 13:24): Email Gateway (Feb 06 2025 at 13:24):From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>
Hi everyone,
The Output dockable now maintains its vertical scroll position. This is very nice and useful and works like a charm.
It does, however, not maintain its horizontal scroll position.
So it loses a bit of its magic when the messages are wider than the Output dockable.
E.g., try to scroll to the end of message 100 while more messages appear - the dockable will always jump back to the beginning of the message:
ML ‹
let
fun write i =
(OS.Process.sleep (seconds 0.2);
Output.writeln
(enclose (string_of_int i) (string_of_int (i*i))
(String.concat (replicate 100 "="))))
in
app write (0 upto 500)
end
›
Best wishes,
Fabian
—
Fabian Immler
fimmler@apple.com
SEG Formal Verification
Email Gateway (Feb 10 2025 at 20:54):From: Makarius <makarius@sketis.net>
On 06/02/2025 14:23, Fabian Immler (via cl-isabelle-users Mailing List) wrote:
The Output dockable now maintains its vertical scroll position.
It does, however, not maintain its horizontal scroll position.
Thank you for testing. I have refined that for current Isabelle2025-RC2.
Note yet posted here, but an open problem: How to make the "divider", the bar
between the search tree and the output, move freely without any implicit
constraints imposed by the overall layout.
Makarius
Last updated: Mar 09 2025 at 12:28 UTC