diff -r 7d1af0a6e797 -r 6e0c0ffb6ec7 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Sep 14 12:46:33 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Sep 14 13:52:16 2012 +0200
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+import java.awt.Color
 import javax.swing.{InputVerifier, JComponent, UIManager}
 import javax.swing.text.JTextComponent
 
@@ -26,6 +27,8 @@
 
 class JEdit_Options extends Options_Variable
 {
+  def color_value(s: String): Color = Color_Value(string(s))
+
   def make_color_component(opt: Options.Opt): Option_Component =
   {
     Swing_Thread.require()