jEdit

Just tried the jEdit 5.0pre1 daily build and attached a screen shot of the
global options panes tree - it's items are still listed in non-alphabetical
order for me.

Robert, are you able to check now?

I guess we understand each other :-) though I cannot verify at this point:

jEdit 4.5 daily shows a fixed order as all versions before.
jEdit 5.0 daily doesn't run at all for me. It hangs with splash at "Migrate
keymaps".

First of all, there is no sorting at all.
There is ordering, however. The order is *NOW* determined by properties in
jedit_gui.props.

This was not being followed by Optional until the recent Optional 1.0.3
release.
And it was hardcoded in jEdit until either 4.5 or 5.0pre1 (can't remember
now).

I can make changes to the property options.group.jedit, for example, and
then I see that same order in the Global Options pane.

Let me know if I am confused about what you are requesting but I think it
is fixed now.

I'd just like to have the same order like You. But I haven't, because
sorting doesn't consider my German labels.

The order seems to be hard-coded or maybe sorted at runtime in a way that
doesn't consider actual labels.

Are you saying you want a new property defined in the .props file so you
can internationalize it and have a different order in the properties?

I like General at top.
The rest are Alphabetical.