src/Tools/jEdit/src/isabelle_options.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 44044 919e2bde7202
child 44699 5199ee17c7d7
permissions -rw-r--r--
propagate editor perspective through document model;
     1 /*  Title:      Tools/jEdit/src/isabelle_options.scala
     2     Author:     Johannes Hölzl, TU Munich
     3 
     4 Editor pane for plugin options.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import javax.swing.JSpinner
    13 
    14 import scala.swing.CheckBox
    15 
    16 import org.gjt.sp.jedit.AbstractOptionPane
    17 
    18 
    19 class Isabelle_Options extends AbstractOptionPane("isabelle")
    20 {
    21   private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
    22   private val auto_start = new CheckBox()
    23   private val relative_font_size = new JSpinner()
    24   private val tooltip_font_size = new JSpinner()
    25   private val tooltip_margin = new JSpinner()
    26   private val tooltip_dismiss_delay = new JSpinner()
    27 
    28   override def _init()
    29   {
    30     addComponent(Isabelle.Property("logic.title"),
    31       logic_selector.peer.asInstanceOf[java.awt.Component])
    32 
    33     addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
    34     auto_start.selected = Isabelle.Boolean_Property("auto-start")
    35 
    36     relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
    37     addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
    38 
    39     tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
    40     addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
    41 
    42     tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
    43     addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
    44 
    45     tooltip_dismiss_delay.setValue(
    46       Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
    47     addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
    48   }
    49 
    50   override def _save()
    51   {
    52     Isabelle.Property("logic") = logic_selector.selection.item.name
    53 
    54     Isabelle.Boolean_Property("auto-start") = auto_start.selected
    55 
    56     Isabelle.Int_Property("relative-font-size") =
    57       relative_font_size.getValue().asInstanceOf[Int]
    58 
    59     Isabelle.Int_Property("tooltip-font-size") =
    60       tooltip_font_size.getValue().asInstanceOf[Int]
    61 
    62     Isabelle.Int_Property("tooltip-margin") =
    63       tooltip_margin.getValue().asInstanceOf[Int]
    64 
    65     Isabelle.Time_Property("tooltip-dismiss-delay") =
    66       Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
    67   }
    68 }