src/Tools/jEdit/src/jedit/isabelle_options.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 src/Tools/jEdit/src/jedit/option_pane.scala@bfea7839d9e1
child 34781 6c2372c4aefb
permissions -rw-r--r--
misc modernization of names;
wenzelm@34407
     1
/*
wenzelm@34408
     2
 * Editor pane for plugin options
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
wenzelm@34407
     5
 */
wenzelm@34407
     6
wenzelm@34318
     7
package isabelle.jedit
wenzelm@34318
     8
wenzelm@34760
     9
wenzelm@34617
    10
import javax.swing.{JComboBox, JSpinner}
wenzelm@34318
    11
wenzelm@34318
    12
import org.gjt.sp.jedit.AbstractOptionPane
wenzelm@34318
    13
wenzelm@34468
    14
wenzelm@34760
    15
class Isabelle_Options extends AbstractOptionPane("isabelle")
wenzelm@34617
    16
{
wenzelm@34617
    17
  private val logic_name = new JComboBox()
wenzelm@34617
    18
  private val font_size = new JSpinner()
wenzelm@34318
    19
wenzelm@34617
    20
  override def _init()
wenzelm@34617
    21
  {
wenzelm@34468
    22
    addComponent(Isabelle.Property("logic.title"), {
wenzelm@34441
    23
      for (name <- Isabelle.system.find_logics()) {
wenzelm@34617
    24
        logic_name.addItem(name)
wenzelm@34468
    25
        if (name == Isabelle.Property("logic"))
wenzelm@34617
    26
          logic_name.setSelectedItem(name)
wenzelm@34318
    27
      }
wenzelm@34617
    28
      logic_name
wenzelm@34617
    29
    })
wenzelm@34617
    30
    addComponent(Isabelle.Property("font-size.title"), {
wenzelm@34617
    31
      font_size.setValue(Isabelle.Int_Property("font-size"))
wenzelm@34617
    32
      font_size
wenzelm@34318
    33
    })
wenzelm@34318
    34
  }
wenzelm@34617
    35
wenzelm@34617
    36
  override def _save()
wenzelm@34617
    37
  {
wenzelm@34617
    38
    val logic = logic_name.getSelectedItem.asInstanceOf[String]
wenzelm@34617
    39
    Isabelle.Property("logic") = logic
wenzelm@34617
    40
wenzelm@34617
    41
    val size = font_size.getValue().asInstanceOf[Int]
wenzelm@34751
    42
    Isabelle.Int_Property("font-size") = size
wenzelm@34318
    43
  }
wenzelm@34318
    44
}