--- a/src/Tools/jEdit/src/jedit_options.scala Wed Sep 12 10:18:31 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Wed Sep 12 11:14:44 2012 +0200
@@ -68,7 +68,13 @@
name = opt_name
val title = opt_title
def load = text = value.check_name(opt_name).value
- def save = update(value + (opt_name, text))
+ def save =
+ try { update(value + (opt_name, text)) }
+ catch {
+ case ERROR(msg) =>
+ Library.error_dialog(this.peer, "Failed to update options",
+ Library.scrollable_text(msg))
+ }
}
text_area.peer.setInputVerifier(new InputVerifier {
def verify(jcomponent: JComponent): Boolean =