--- 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()