wenzelm@43282: /*  Title:      Tools/jEdit/src/isabelle_options.scala
wenzelm@36760:     Author:     Johannes Hölzl, TU Munich
wenzelm@36760: 
wenzelm@36760: Editor pane for plugin options.
wenzelm@36760: */
wenzelm@34407: 
wenzelm@34318: package isabelle.jedit
wenzelm@34318: 
wenzelm@34760: 
wenzelm@40850: import isabelle._
wenzelm@40850: 
wenzelm@39518: import javax.swing.JSpinner
wenzelm@34318: 
wenzelm@39734: import scala.swing.CheckBox
wenzelm@39734: 
wenzelm@34318: import org.gjt.sp.jedit.AbstractOptionPane
wenzelm@34318: 
wenzelm@34468: 
wenzelm@34760: class Isabelle_Options extends AbstractOptionPane("isabelle")
wenzelm@34617: {
wenzelm@39517:   private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
wenzelm@39734:   private val auto_start = new CheckBox()
wenzelm@36814:   private val relative_font_size = new JSpinner()
wenzelm@37201:   private val tooltip_font_size = new JSpinner()
wenzelm@40339:   private val tooltip_margin = new JSpinner()
wenzelm@38854:   private val tooltip_dismiss_delay = new JSpinner()
wenzelm@34318: 
wenzelm@34617:   override def _init()
wenzelm@34617:   {
wenzelm@44044:     addComponent(Isabelle.Property("logic.title"),
wenzelm@44044:       logic_selector.peer.asInstanceOf[java.awt.Component])
wenzelm@34782: 
wenzelm@39734:     addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
wenzelm@39734:     auto_start.selected = Isabelle.Boolean_Property("auto-start")
wenzelm@39734: 
wenzelm@39734:     relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
wenzelm@39734:     addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
wenzelm@37201: 
wenzelm@39734:     tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
wenzelm@39734:     addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
wenzelm@38854: 
wenzelm@40339:     tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
wenzelm@40339:     addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
wenzelm@40339: 
wenzelm@40849:     tooltip_dismiss_delay.setValue(
wenzelm@40850:       Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
wenzelm@39734:     addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
wenzelm@34318:   }
wenzelm@34617: 
wenzelm@34617:   override def _save()
wenzelm@34617:   {
wenzelm@39734:     Isabelle.Property("logic") = logic_selector.selection.item.name
wenzelm@39734: 
wenzelm@39734:     Isabelle.Boolean_Property("auto-start") = auto_start.selected
wenzelm@34617: 
wenzelm@36814:     Isabelle.Int_Property("relative-font-size") =
wenzelm@36814:       relative_font_size.getValue().asInstanceOf[Int]
wenzelm@37201: 
wenzelm@37201:     Isabelle.Int_Property("tooltip-font-size") =
wenzelm@37201:       tooltip_font_size.getValue().asInstanceOf[Int]
wenzelm@38854: 
wenzelm@40339:     Isabelle.Int_Property("tooltip-margin") =
wenzelm@40339:       tooltip_margin.getValue().asInstanceOf[Int]
wenzelm@40339: 
wenzelm@40850:     Isabelle.Time_Property("tooltip-dismiss-delay") =
wenzelm@40850:       Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
wenzelm@34318:   }
wenzelm@34318: }