src/Tools/jEdit/src/jedit_options.scala

     def load() { selected = stored }
     load()
   }
 }
 
-class JEdit_Options extends Options_Variable
+class JEdit_Options(init_options: Options) extends Options_Variable(init_options)
 {
   def color_value(s: String): Color = Color_Value(string(s))
 
   def make_color_component(opt: Options.Opt): Option_Component =
   {

             if (default_font != null) font = default_font
             name = opt_name
             val title = opt_title
             def load = text = value.check_name(opt_name).value
             def save =
-              try { store(value + (opt_name, text)) }
+              try { JEdit_Options.this += (opt_name, text) }
               catch {
                 case ERROR(msg) =>
                   GUI.error_dialog(this.peer, "Failed to update options",
                     GUI.scrollable_text(msg))
               }