# HG changeset patch
# User wenzelm
# Date 1347398763 -7200
# Node ID 313369027391c150b42ff04e564f0d85e0f31871
# Parent  2750756db9c56b13972a27bffc73769f58f9bd00
some GUI support for color options;

diff -r 2750756db9c5 -r 313369027391 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Sep 11 22:59:25 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Sep 11 23:26:03 2012 +0200
@@ -150,7 +150,7 @@
 
 
 final class Options private(
-  protected val options: Map[String, Options.Opt] = Map.empty,
+  val options: Map[String, Options.Opt] = Map.empty,
   val section: String = "")
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")
diff -r 2750756db9c5 -r 313369027391 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Sep 11 22:59:25 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 23:26:03 2012 +0200
@@ -19,7 +19,7 @@
   -- "global delay for Swing tooltips"
 
 
-section "Editor Document View"
+section "Rendering of Document Content"
 
 option color_outdated : string = "EEE3E3FF"
 option color_unprocessed : string = "FFA0A0FF"
diff -r 2750756db9c5 -r 313369027391 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 22:59:25 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 23:26:03 2012 +0200
@@ -22,8 +22,15 @@
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 
-  private val components =
-    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
+  private val predefined =
+    Isabelle_Logic.logic_selector(false) ::
+      (for {
+        (name, opt) <- Isabelle.options.value.options.toList
+        // FIXME avoid hard-wired stuff
+        if (name.startsWith("color_") && opt.section == "Rendering of Document Content")
+      } yield Isabelle.options.make_color_component(opt))
+
+  private val components = Isabelle.options.make_components(predefined, relevant_options)
 
   override def _init()
   {
diff -r 2750756db9c5 -r 313369027391 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 22:59:25 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 23:26:03 2012 +0200
@@ -14,6 +14,8 @@
 
 import scala.swing.{Component, CheckBox, TextArea}
 
+import org.gjt.sp.jedit.gui.ColorWellButton
+
 
 trait Option_Component extends Component
 {
@@ -24,6 +26,25 @@
 
 class JEdit_Options extends Options_Variable
 {
+  def make_color_component(opt: Options.Opt): Option_Component =
+  {
+    Swing_Thread.require()
+
+    val opt_name = opt.name
+    val opt_title = opt.title("jedit")
+
+    val button = new ColorWellButton(Color_Value(opt.value))
+    val component = new Component with Option_Component {
+      override lazy val peer = button
+      name = opt_name
+      val title = opt_title
+      def load = button.setSelectedColor(Color_Value(string(opt_name)))
+      def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
+    }
+    component.tooltip = Isabelle.tooltip(opt.print_default)
+    component
+  }
+
   def make_component(opt: Options.Opt): Option_Component =
   {
     Swing_Thread.require()