src/Tools/jEdit/src/jedit/isabelle_options.scala
author wenzelm
Tue, 11 May 2010 15:47:31 +0200
changeset 36814 dc85664dbf6d
parent 36760 b82a698ef6c9
child 36817 ed97e877ff2d
permissions -rw-r--r--
support Isabelle plugin properties with defaults; font size relative to view.textsize of jEdit; margin relative to component width and approximative font metrics;

/*  Title:      Tools/jEdit/src/jedit/isabelle_options.scala
    Author:     Johannes Hölzl, TU Munich

Editor pane for plugin options.
*/

package isabelle.jedit


import javax.swing.{JComboBox, JSpinner}

import org.gjt.sp.jedit.AbstractOptionPane


class Isabelle_Options extends AbstractOptionPane("isabelle")
{
  private val logic_name = new JComboBox()
  private val relative_font_size = new JSpinner()
  private val relative_margin = new JSpinner()

  private class List_Item(val name: String, val descr: String) {
    def this(name: String) = this(name, name)
    override def toString = descr
  }

  override def _init()
  {
    val logic = Isabelle.Property("logic")
    addComponent(Isabelle.Property("logic.title"), {
      logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
      for (name <- Isabelle.system.find_logics()) {
        val item = new List_Item(name)
        logic_name.addItem(item)
        if (name == logic)
          logic_name.setSelectedItem(item)
      }
      logic_name
    })

    addComponent(Isabelle.Property("relative-font-size.title"), {
      relative_font_size.setValue(Isabelle.Int_Property("relative-font-size"))
      relative_font_size
    })

    addComponent(Isabelle.Property("relative-margin.title"), {
      relative_margin.setValue(Isabelle.Int_Property("relative-margin"))
      relative_margin
    })
  }

  override def _save()
  {
    Isabelle.Property("logic") =
      logic_name.getSelectedItem.asInstanceOf[List_Item].name

    Isabelle.Int_Property("relative-font-size") =
      relative_font_size.getValue().asInstanceOf[Int]

    Isabelle.Int_Property("relative-margin") =
      relative_margin.getValue().asInstanceOf[Int]
  }
}