some GUI support for color options;
authorwenzelm
Tue Sep 11 23:26:03 2012 +0200 (2012-09-11)
changeset 49296313369027391
parent 49295 2750756db9c5
child 49299 f9f240dfb50b
some GUI support for color options;
src/Pure/System/options.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/jedit_options.scala
     1.1 --- a/src/Pure/System/options.scala	Tue Sep 11 22:59:25 2012 +0200
     1.2 +++ b/src/Pure/System/options.scala	Tue Sep 11 23:26:03 2012 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4  
     1.5  
     1.6  final class Options private(
     1.7 -  protected val options: Map[String, Options.Opt] = Map.empty,
     1.8 +  val options: Map[String, Options.Opt] = Map.empty,
     1.9    val section: String = "")
    1.10  {
    1.11    override def toString: String = options.iterator.mkString("Options (", ",", ")")
     2.1 --- a/src/Tools/jEdit/etc/options	Tue Sep 11 22:59:25 2012 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Tue Sep 11 23:26:03 2012 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4    -- "global delay for Swing tooltips"
     2.5  
     2.6  
     2.7 -section "Editor Document View"
     2.8 +section "Rendering of Document Content"
     2.9  
    2.10  option color_outdated : string = "EEE3E3FF"
    2.11  option color_unprocessed : string = "FFA0A0FF"
     3.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 22:59:25 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 23:26:03 2012 +0200
     3.3 @@ -22,8 +22,15 @@
     3.4  
     3.5    relevant_options.foreach(Isabelle.options.value.check_name _)
     3.6  
     3.7 -  private val components =
     3.8 -    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
     3.9 +  private val predefined =
    3.10 +    Isabelle_Logic.logic_selector(false) ::
    3.11 +      (for {
    3.12 +        (name, opt) <- Isabelle.options.value.options.toList
    3.13 +        // FIXME avoid hard-wired stuff
    3.14 +        if (name.startsWith("color_") && opt.section == "Rendering of Document Content")
    3.15 +      } yield Isabelle.options.make_color_component(opt))
    3.16 +
    3.17 +  private val components = Isabelle.options.make_components(predefined, relevant_options)
    3.18  
    3.19    override def _init()
    3.20    {
     4.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 22:59:25 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 23:26:03 2012 +0200
     4.3 @@ -14,6 +14,8 @@
     4.4  
     4.5  import scala.swing.{Component, CheckBox, TextArea}
     4.6  
     4.7 +import org.gjt.sp.jedit.gui.ColorWellButton
     4.8 +
     4.9  
    4.10  trait Option_Component extends Component
    4.11  {
    4.12 @@ -24,6 +26,25 @@
    4.13  
    4.14  class JEdit_Options extends Options_Variable
    4.15  {
    4.16 +  def make_color_component(opt: Options.Opt): Option_Component =
    4.17 +  {
    4.18 +    Swing_Thread.require()
    4.19 +
    4.20 +    val opt_name = opt.name
    4.21 +    val opt_title = opt.title("jedit")
    4.22 +
    4.23 +    val button = new ColorWellButton(Color_Value(opt.value))
    4.24 +    val component = new Component with Option_Component {
    4.25 +      override lazy val peer = button
    4.26 +      name = opt_name
    4.27 +      val title = opt_title
    4.28 +      def load = button.setSelectedColor(Color_Value(string(opt_name)))
    4.29 +      def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
    4.30 +    }
    4.31 +    component.tooltip = Isabelle.tooltip(opt.print_default)
    4.32 +    component
    4.33 +  }
    4.34 +
    4.35    def make_component(opt: Options.Opt): Option_Component =
    4.36    {
    4.37      Swing_Thread.require()