[ jEdit-devel ] [Q] Plugin data persistence

[Art T. <ree...@as...>]

I whipped up a quick plugin to manage a todo list, and I was wondering
about the proper jedit idiom for persisting plugin data.  I was tempted
to open my own file within the settings directory, but didn't want to
waste the time with Java's annoying IO model if there's a better way.

What I ended up doing was serialising out list items into a single
string, and storing that in the user properties.  I have two questions
related to this solution: is there a limit, practical or explicit, on
the length of a property value?  Is there a mechanism to retrieve the
"user properties" mentioned in the documentation, or is the
getProperties() call the appropriate mechanism for this?

If anyone cares to check it out, I have it up at
http://www.astrogoth.com/~reeses/software.  I haven't bothered to clean
up the code at all, and this was a "teach myself that silly java gui
stuff" exercise more than anything.  I also don't have a firm handle on
the various plugin properties, so expect some ugliness.

Thanks.

-a.