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