src/Tools/jEdit/src/jedit_options.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62227 6eeaaefcea56
child 65236 4fa82bbb394e
permissions -rw-r--r--
tuned signature;
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@61607
    12
import java.awt.{Font, Color}
wenzelm@49252
    13
import javax.swing.{InputVerifier, JComponent, UIManager}
wenzelm@49246
    14
import javax.swing.text.JTextComponent
wenzelm@49252
    15
wenzelm@49246
    16
import scala.swing.{Component, CheckBox, TextArea}
wenzelm@60843
    17
import scala.swing.event.ButtonClicked
wenzelm@49246
    18
wenzelm@49296
    19
import org.gjt.sp.jedit.gui.ColorWellButton
wenzelm@49296
    20
wenzelm@49246
    21
wenzelm@49246
    22
trait Option_Component extends Component
wenzelm@49246
    23
{
wenzelm@49246
    24
  val title: String
wenzelm@49247
    25
  def load(): Unit
wenzelm@49246
    26
  def save(): Unit
wenzelm@49246
    27
}
wenzelm@49245
    28
wenzelm@52065
    29
object JEdit_Options
wenzelm@52065
    30
{
wenzelm@52065
    31
  val RENDERING_SECTION = "Rendering of Document Content"
wenzelm@60843
    32
wenzelm@60843
    33
  class Check_Box(name: String, label: String, description: String) extends CheckBox(label)
wenzelm@60843
    34
  {
wenzelm@60843
    35
    tooltip = description
wenzelm@60843
    36
    reactions += { case ButtonClicked(_) => update(selected) }
wenzelm@60843
    37
wenzelm@60843
    38
    def stored: Boolean = PIDE.options.bool(name)
wenzelm@60843
    39
    def update(b: Boolean): Unit =
wenzelm@60843
    40
      GUI_Thread.require {
wenzelm@60843
    41
        if (selected != b) selected = b
wenzelm@60843
    42
        if (stored != b) {
wenzelm@60843
    43
          PIDE.options.bool(name) = b
wenzelm@60843
    44
          PIDE.session.update_options(PIDE.options.value)
wenzelm@60843
    45
        }
wenzelm@60843
    46
      }
wenzelm@60844
    47
    def load() { selected = stored }
wenzelm@60844
    48
    load()
wenzelm@60843
    49
  }
wenzelm@52065
    50
}
wenzelm@52065
    51
wenzelm@49245
    52
class JEdit_Options extends Options_Variable
wenzelm@49245
    53
{
wenzelm@49356
    54
  def color_value(s: String): Color = Color_Value(string(s))
wenzelm@49356
    55
wenzelm@49296
    56
  def make_color_component(opt: Options.Opt): Option_Component =
wenzelm@49296
    57
  {
wenzelm@57612
    58
    GUI_Thread.require {}
wenzelm@49296
    59
wenzelm@49296
    60
    val opt_name = opt.name
wenzelm@49296
    61
    val opt_title = opt.title("jedit")
wenzelm@49296
    62
wenzelm@49296
    63
    val button = new ColorWellButton(Color_Value(opt.value))
wenzelm@49296
    64
    val component = new Component with Option_Component {
wenzelm@49296
    65
      override lazy val peer = button
wenzelm@49296
    66
      name = opt_name
wenzelm@49296
    67
      val title = opt_title
wenzelm@49296
    68
      def load = button.setSelectedColor(Color_Value(string(opt_name)))
wenzelm@49296
    69
      def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
wenzelm@49296
    70
    }
wenzelm@56622
    71
    component.tooltip = GUI.tooltip_lines(opt.print_default)
wenzelm@49296
    72
    component
wenzelm@49296
    73
  }
wenzelm@49296
    74
wenzelm@49270
    75
  def make_component(opt: Options.Opt): Option_Component =
wenzelm@49246
    76
  {
wenzelm@57612
    77
    GUI_Thread.require {}
wenzelm@49246
    78
wenzelm@49270
    79
    val opt_name = opt.name
wenzelm@49270
    80
    val opt_title = opt.title("jedit")
wenzelm@49246
    81
wenzelm@49246
    82
    val component =
wenzelm@49246
    83
      if (opt.typ == Options.Bool)
wenzelm@49246
    84
        new CheckBox with Option_Component {
wenzelm@49270
    85
          name = opt_name
wenzelm@49246
    86
          val title = opt_title
wenzelm@49247
    87
          def load = selected = bool(opt_name)
wenzelm@49246
    88
          def save = bool(opt_name) = selected
wenzelm@49246
    89
        }
wenzelm@49246
    90
      else {
wenzelm@61742
    91
        val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
wenzelm@49246
    92
        val text_area =
wenzelm@49246
    93
          new TextArea with Option_Component {
wenzelm@61742
    94
            if (default_font != null) font = default_font
wenzelm@49270
    95
            name = opt_name
wenzelm@49246
    96
            val title = opt_title
wenzelm@49247
    97
            def load = text = value.check_name(opt_name).value
wenzelm@49317
    98
            def save =
wenzelm@62227
    99
              try { store(value + (opt_name, text)) }
wenzelm@49317
   100
              catch {
wenzelm@49317
   101
                case ERROR(msg) =>
wenzelm@51616
   102
                  GUI.error_dialog(this.peer, "Failed to update options",
wenzelm@51616
   103
                    GUI.scrollable_text(msg))
wenzelm@49317
   104
              }
wenzelm@49246
   105
          }
wenzelm@49246
   106
        text_area.peer.setInputVerifier(new InputVerifier {
wenzelm@49246
   107
          def verify(jcomponent: JComponent): Boolean =
wenzelm@49246
   108
            jcomponent match {
wenzelm@49246
   109
              case text: JTextComponent =>
wenzelm@49246
   110
                try { value + (opt_name, text.getText); true }
wenzelm@49246
   111
                catch { case ERROR(_) => false }
wenzelm@49246
   112
              case _ => true
wenzelm@49246
   113
            }
wenzelm@49246
   114
          })
wenzelm@56752
   115
        GUI.plain_focus_traversal(text_area.peer)
wenzelm@49246
   116
        text_area
wenzelm@49246
   117
      }
wenzelm@49247
   118
    component.load()
wenzelm@56622
   119
    component.tooltip = GUI.tooltip_lines(opt.print_default)
wenzelm@49246
   120
    component
wenzelm@49246
   121
  }
wenzelm@49270
   122
wenzelm@49270
   123
  def make_components(predefined: List[Option_Component], filter: String => Boolean)
wenzelm@49270
   124
    : List[(String, List[Option_Component])] =
wenzelm@49270
   125
  {
wenzelm@49270
   126
    def mk_component(opt: Options.Opt): List[Option_Component] =
wenzelm@49270
   127
      predefined.find(opt.name == _.name) match {
wenzelm@49270
   128
        case Some(c) => List(c)
wenzelm@49270
   129
        case None => if (filter(opt.name)) List(make_component(opt)) else Nil
wenzelm@49270
   130
      }
wenzelm@49270
   131
    value.sections.sortBy(_._1).map(
wenzelm@49270
   132
        { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component _)) })
wenzelm@49270
   133
      .filterNot(_._2.isEmpty)
wenzelm@49270
   134
  }
wenzelm@49245
   135
}
wenzelm@49245
   136