[ jEdit-devel ] [ jedit-Feature Requests-2919873 ] Searchable options

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

Feature Requests item #2919873, was opened at 2009-12-23 08:09
Message generated for change (Tracker Item Submitted) made by thiemo
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=350588&aid=2919873&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: core
Group: None
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: Thiemo Kellner (thiemo)
Assigned to: Nobody/Anonymous (nobody)
Summary: Searchable options

Initial Comment:
It would be nice if the option panes had a search functionality one would locate the option containing the searched string. If the result was clickable like the hyper search such that the clicked option finding would be focussed and highlighted, it would add additional comfort. I think alongside TOAD and attached a screen shot of their solution.

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

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