On Mon, 11 Jul 2011, Christian Sternagel wrote:

- I love Ctrl-click for looking up definitions and lemmas. Is there a way of jumping back to where I came from (I mean the exact position of the cursor)?

Not yet. The hyperlink jumps into the dark, crashing at the target (the other file is not integrated properly into the current document model). There are several races from the way the Hyperlinks plugin is doing it, and no way back so far.


- I guess this is Java-specific but I mention it anyway: On my system (fedora 15 + Gnome 3) there is the "feature" of snapping windows to the right or left or top (such that they will occupy the right-half, the left-half, or the full screen). After doing that, however, the menu does no longer work properly when navigated by the mouse, i.e., it does open at a wrong position of the screen (strangely, everything works fine with keyboard shortcuts).

Which desktop manager is that, and which feature of it? If it is a general Java + jEdit issue, you can post that on one of the jedit mailing lists or trackers. (If it is OpenJDK again, I think the jedit maintainers will just ignore it, though.)


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to