Email Gateway (Aug 22 2022 at 16:01): Email Gateway (Aug 22 2022 at 16:01):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
If I am working with the cursor at a particular position in a theory,
then I double click on the sidebar to switch to a theory, and then I
double click to return to the original theory, I do not return to the
original editing position, but rather to the top of the buffer.
Email Gateway (Aug 22 2022 at 16:02):From: Makarius <makarius@sketis.net>
What means "sidebar" here?
I have experimented a bit with the jEdit buffer switcher at the top, the
jEdit file-browser dockable, and the Isabelle/jEdit Theories dockable to
go back and forth between various theories. Cursor positions are
preserved as expected.
Can you reproduce the problem with clean user properties? E.g. while the
application is shutdown you can rename the $ISABELLE_HOME_USER/jedit
directory and then start the application afresh.
Makarius
Email Gateway (Aug 22 2022 at 16:02):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
By "double click on the sidebar" I meant: "double click on one of the
theory buttons shown in the 'Theories' panel that by default is docked
on the right-hand side of the UI."
To repeat the problem with clean user properties, I renamed aside
the entire ~/.isabelle/Isabelle2017-RC1 folder with the application not
running. Then I started the application:
/opt/Isabelle2017-RC1/Isabelle2017-RC1&
I waited for it to build the HOL heap (I normally use x86-64, so I guess
it had to build it for x86). Then I used the File>Open to open one
of my theory files that imported some other theory files, so that at
the end I had several buttons listed in the "Theories" panel docked
at the right. In one of the theories I scroll down and click to position
the cursor at a location somewhere in the middle of the theory.
Then I double click on one of the other theory buttons, and the main
editor window contents change to show that. Then I double click on the
button corresponding to the original theory and the view is positioned
at the beginning of the theory, not at the location where I had
positioned the cursor before switching away.
Email Gateway (Aug 22 2022 at 16:02):From: Makarius <makarius@sketis.net>
OK. I've managed to get the described effect, and improved the situation
here
http://isabelle.in.tum.de/repos/isabelle/rev/261dcd52c5a0
Makarius
Last updated: Apr 27 2024 at 04:17 UTC