--- 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 (", ",", ")")
--- 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"
--- 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()
{
--- 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()