[ jEdit-devel ] [ jedit-Plugin Feature Requests-3006101 ] MarkerSets: Highlight current marker after next/prev

[SourceForge.net <no...@so...>]

Plugin Feature Requests item #3006101, was opened at 2010-05-23 21:52
Message generated for change (Comment added) made by shlomy
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=997936&aid=3006101&group_id=588

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: None
Group: None
>Status: Closed
Priority: 5
Private: No
Submitted By: Alan Ezust (ezust)
Assigned to: Shlomy Reinstein (shlomy)
Summary: MarkerSets: Highlight current marker after next/prev

Initial Comment:
It would be nice if after a keyboard action that invokes next/previous marker, that the Marker Sets dockable would highlight the currently displayed marker. 



----------------------------------------------------------------------

>Comment By: Shlomy Reinstein (shlomy)
Date: 2011-07-18 22:20

Message:
Implemented in version 47349da..d90f990.
There is a strange problem, I think the markerset retains the order the
markers were added to it, so next/prev can cause jumps in the dockable. But
this is another issue, which could also be seen by pressing the next/prev
arrows in the dockable, unrelated to this feature request.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=997936&aid=3006101&group_id=588