src/Tools/jEdit/src/jedit_options.scala
author wenzelm
Tue Sep 11 15:47:42 2012 +0200 (2012-09-11)
changeset 49270 e5d162d15867
parent 49252 9e10481dd3c4
child 49289 60424f123621
permissions -rw-r--r--
some support to organize options in sections;
wenzelm@49245
     1
/*  Title:      Tools/jEdit/src/jedit_options.scala
wenzelm@49245
     2
    Author:     Makarius
wenzelm@49245
     3
wenzelm@49245
     4
Options for Isabelle/jEdit.
wenzelm@49245
     5
*/
wenzelm@49245
     6
wenzelm@49245
     7
package isabelle.jedit
wenzelm@49245
     8
wenzelm@49245
     9
wenzelm@49245
    10
import isabelle._
wenzelm@49245
    11
wenzelm@49252
    12
import javax.swing.{InputVerifier, JComponent, UIManager}
wenzelm@49246
    13
import javax.swing.text.JTextComponent
wenzelm@49252
    14
wenzelm@49246
    15
import scala.swing.{Component, CheckBox, TextArea}
wenzelm@49246
    16
wenzelm@49246
    17
wenzelm@49246
    18
trait Option_Component extends Component
wenzelm@49246
    19
{
wenzelm@49246
    20
  val title: String
wenzelm@49247
    21
  def load(): Unit
wenzelm@49246
    22
  def save(): Unit
wenzelm@49246
    23
}
wenzelm@49245
    24
wenzelm@49245
    25
class JEdit_Options extends Options_Variable
wenzelm@49245
    26
{
wenzelm@49270
    27
  def make_component(opt: Options.Opt): Option_Component =
wenzelm@49246
    28
  {
wenzelm@49246
    29
    Swing_Thread.require()
wenzelm@49246
    30
wenzelm@49270
    31
    val opt_name = opt.name
wenzelm@49270
    32
    val opt_title = opt.title("jedit")
wenzelm@49246
    33
wenzelm@49246
    34
    val component =
wenzelm@49246
    35
      if (opt.typ == Options.Bool)
wenzelm@49246
    36
        new CheckBox with Option_Component {
wenzelm@49270
    37
          name = opt_name
wenzelm@49246
    38
          val title = opt_title
wenzelm@49247
    39
          def load = selected = bool(opt_name)
wenzelm@49246
    40
          def save = bool(opt_name) = selected
wenzelm@49246
    41
        }
wenzelm@49246
    42
      else {
wenzelm@49252
    43
        val default_font = UIManager.getFont("TextField.font")
wenzelm@49246
    44
        val text_area =
wenzelm@49246
    45
          new TextArea with Option_Component {
wenzelm@49252
    46
            if (default_font != null) font = default_font
wenzelm@49270
    47
            name = opt_name
wenzelm@49246
    48
            val title = opt_title
wenzelm@49247
    49
            def load = text = value.check_name(opt_name).value
wenzelm@49246
    50
            def save = update(value + (opt_name, text))
wenzelm@49246
    51
          }
wenzelm@49246
    52
        text_area.peer.setInputVerifier(new InputVerifier {
wenzelm@49246
    53
          def verify(jcomponent: JComponent): Boolean =
wenzelm@49246
    54
            jcomponent match {
wenzelm@49246
    55
              case text: JTextComponent =>
wenzelm@49246
    56
                try { value + (opt_name, text.getText); true }
wenzelm@49246
    57
                catch { case ERROR(_) => false }
wenzelm@49246
    58
              case _ => true
wenzelm@49246
    59
            }
wenzelm@49246
    60
          })
wenzelm@49246
    61
        text_area
wenzelm@49246
    62
      }
wenzelm@49247
    63
    component.load()
wenzelm@49248
    64
    component.tooltip = Isabelle.tooltip(opt.print)
wenzelm@49246
    65
    component
wenzelm@49246
    66
  }
wenzelm@49270
    67
wenzelm@49270
    68
  def make_components(predefined: List[Option_Component], filter: String => Boolean)
wenzelm@49270
    69
    : List[(String, List[Option_Component])] =
wenzelm@49270
    70
  {
wenzelm@49270
    71
    def mk_component(opt: Options.Opt): List[Option_Component] =
wenzelm@49270
    72
      predefined.find(opt.name == _.name) match {
wenzelm@49270
    73
        case Some(c) => List(c)
wenzelm@49270
    74
        case None => if (filter(opt.name)) List(make_component(opt)) else Nil
wenzelm@49270
    75
      }
wenzelm@49270
    76
    value.sections.sortBy(_._1).map(
wenzelm@49270
    77
        { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component _)) })
wenzelm@49270
    78
      .filterNot(_._2.isEmpty)
wenzelm@49270
    79
  }
wenzelm@49245
    80
}
wenzelm@49245
    81