tuned error;
authorwenzelm
Wed, 12 Sep 2012 11:14:44 +0200
changeset 49317 5eff42e69edb
parent 49316 a1b0654e7c90
child 49318 612a04e7c853
tuned error;
src/Tools/jEdit/src/jedit_options.scala
--- 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 =