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;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/isabelle_options.scala
wenzelm@36760
     2
    Author:     Johannes Hölzl, TU Munich
wenzelm@36760
     3
wenzelm@36760
     4
Editor pane for plugin options.
wenzelm@36760
     5
*/
wenzelm@34407
     6
wenzelm@34318
     7
package isabelle.jedit
wenzelm@34318
     8
wenzelm@34760
     9
wenzelm@40850
    10
import isabelle._
wenzelm@40850
    11
wenzelm@39518
    12
import javax.swing.JSpinner
wenzelm@34318
    13
wenzelm@39734
    14
import scala.swing.CheckBox
wenzelm@39734
    15
wenzelm@34318
    16
import org.gjt.sp.jedit.AbstractOptionPane
wenzelm@34318
    17
wenzelm@34468
    18
wenzelm@34760
    19
class Isabelle_Options extends AbstractOptionPane("isabelle")
wenzelm@34617
    20
{
wenzelm@39517
    21
  private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
wenzelm@39734
    22
  private val auto_start = new CheckBox()
wenzelm@36814
    23
  private val relative_font_size = new JSpinner()
wenzelm@37201
    24
  private val tooltip_font_size = new JSpinner()
wenzelm@40339
    25
  private val tooltip_margin = new JSpinner()
wenzelm@38854
    26
  private val tooltip_dismiss_delay = new JSpinner()
wenzelm@34318
    27
wenzelm@34617
    28
  override def _init()
wenzelm@34617
    29
  {
wenzelm@44044
    30
    addComponent(Isabelle.Property("logic.title"),
wenzelm@44044
    31
      logic_selector.peer.asInstanceOf[java.awt.Component])
wenzelm@34782
    32
wenzelm@39734
    33
    addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
wenzelm@39734
    34
    auto_start.selected = Isabelle.Boolean_Property("auto-start")
wenzelm@39734
    35
wenzelm@39734
    36
    relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
wenzelm@39734
    37
    addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
wenzelm@37201
    38
wenzelm@39734
    39
    tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
wenzelm@39734
    40
    addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
wenzelm@38854
    41
wenzelm@40339
    42
    tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
wenzelm@40339
    43
    addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
wenzelm@40339
    44
wenzelm@40849
    45
    tooltip_dismiss_delay.setValue(
wenzelm@40850
    46
      Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
wenzelm@39734
    47
    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
wenzelm@34318
    48
  }
wenzelm@34617
    49
wenzelm@34617
    50
  override def _save()
wenzelm@34617
    51
  {
wenzelm@39734
    52
    Isabelle.Property("logic") = logic_selector.selection.item.name
wenzelm@39734
    53
wenzelm@39734
    54
    Isabelle.Boolean_Property("auto-start") = auto_start.selected
wenzelm@34617
    55
wenzelm@36814
    56
    Isabelle.Int_Property("relative-font-size") =
wenzelm@36814
    57
      relative_font_size.getValue().asInstanceOf[Int]
wenzelm@37201
    58
wenzelm@37201
    59
    Isabelle.Int_Property("tooltip-font-size") =
wenzelm@37201
    60
      tooltip_font_size.getValue().asInstanceOf[Int]
wenzelm@38854
    61
wenzelm@40339
    62
    Isabelle.Int_Property("tooltip-margin") =
wenzelm@40339
    63
      tooltip_margin.getValue().asInstanceOf[Int]
wenzelm@40339
    64
wenzelm@40850
    65
    Isabelle.Time_Property("tooltip-dismiss-delay") =
wenzelm@40850
    66
      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
wenzelm@34318
    67
  }
wenzelm@34318
    68
}