#182 would like to be able to save groups of settings
Situation: I've got a single laptop that I use as both a work
machine and for presentations in class. When I use DrJava
for demos in class, I need to use larger fonts so the
projected image is visible in the back of the room. When
I'm using it for work, I want regular-sized, smaller fonts so
more information fits on the screen.
It would be very nice if there were some way to save sets
of preference settings and switch rapidly between them,
instead of having to change individual options one by one,
and remember the particular settings used in each
situation.
My particular situation only involves font settings, but it
might be useful to implement this in a fairly general way so
it doesn't restrict people to just a small, hard-wired set of
preference settings that can be included in a saved set.
Logged In: YES
user_id=429731
There was some discussion earlier about being able to import
and export preferences to a file, which would be a good
first step for this. But I agree-- having the ability to
selectively export would be even more valuable. Perhaps it
could be done at the granularity of a "group" of settings?
Or maybe a tree of checkboxes (initially collapsed) could be
displayed, allowing the user to select a group at a time, or
to drill down and turn individual options on or off.
Some other great uses for this: saving color settings (like
Peter's white text on black background) and key bindings
(eg. Emacs binidngs), which could even be provided on the
DrJava web site as resources for people to download.
Implementation notes for the developers:
I remember looking at this briefly, and being surprised that
the FileConfiguration object doesn't appear to have the
ability to load in extra changes after it has been created
(if I remember correctly). This would be a good refactoring
project with obvious unit tests.
Charlie
Logged In: YES
user_id=431096
There is a much, much simpler solution to this problem. All of
DrJava's settings are saved to a ".drjava" file in your home
directory (wherever Java tells us that is). Just copy the file,
change the settings you want, and then swap between the two
files. Two lines of shell script should take care of it.
As for the more complex solution, I frankly don't like it. It adds
unnecessary complexity to an already complex preference system.
It would be nice to have all of the features Theo originally
designed for the config framework (nested Configurations, passing
calls through a la the classloader design), but at the time we
decided that it wasn't important enough to finish. I still think that's
true. The current system works for most users, and there are
simple workarounds for most other problems. My $5.02.
Logged In: YES
user_id=728235
Fumbling around with the .drjava files is a fairly clumsy way to do
this. What I had in mind was more along the lines of the old
Apple network configuration collections. Normally there was
nothing special about the settings; they were saved as the
"default" settings. But you could pick "save settings as..." (or
something similar) from the settings popup menu and pick a
name for the current group of settings. After that, the newly
named settings were available as one of the options in that popup
menu.
Essentially what they were doing was to maintain parallel sets of
preference files that could be switched instantly instead of
renaming files. In DrJava's case I think you could have a .drjava-
xyzzy file for an option set named xyzzy, and reload as needed
when the user switches sets.
This would be a nice convenience, but isn't a terribly high-priority
thing, so I don't want to push it too hard if it really is that difficult
or would really complicate the user interface.
Logged In: YES
user_id=728235
Fumbling around with the .drjava files is a fairly clumsy way to do
this. What I had in mind was more along the lines of the old
Apple network configuration collections. Normally there was
nothing special about the settings; they were saved as the
"default" settings. But you could pick "save settings as..." (or
something similar) from the settings popup menu and pick a
name for the current group of settings. After that, the newly
named settings were available as one of the options in that popup
menu.
Essentially what they were doing was to maintain parallel sets of
preference files that could be switched instantly instead of
renaming files. In DrJava's case I think you could have a .drjava-
xyzzy file for an option set named xyzzy, and reload as needed
when the user switches sets.
This would be a nice convenience, but isn't a terribly high-priority
thing, so I don't want to push it too hard if it really is that difficult
or would really complicate the user interface.
Logged In: YES
user_id=1075744
Originator: NO
We could probably add something like this as part of the planned "external tools" facility.