src/Tools/jEdit/src/isabelle_options.scala
author wenzelm
Tue Mar 07 14:33:14 2017 +0100 (2017-03-07)
changeset 65139 0a2c0712e432
parent 62973 744266e32612
child 65256 c3d6dd17d626
permissions -rw-r--r--
clarified modules: spell-checker in Pure;
     1 /*  Title:      Tools/jEdit/src/isabelle_options.scala
     2     Author:     Makarius
     3 
     4 Editor pane for plugin options.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
    13 
    14 
    15 abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name)
    16 {
    17   protected val components: List[(String, List[Option_Component])]
    18 
    19   override def _init()
    20   {
    21     val dummy_property = "options.isabelle.dummy"
    22 
    23     for ((s, cs) <- components) {
    24       if (s != "") {
    25         jEdit.setProperty(dummy_property, s)
    26         addSeparator(dummy_property)
    27         jEdit.setProperty(dummy_property, null)
    28       }
    29       cs.foreach(c => addComponent(c.title, c.peer))
    30     }
    31   }
    32 
    33   override def _save()
    34   {
    35     for ((_, cs) <- components) cs.foreach(_.save())
    36   }
    37 }
    38 
    39 
    40 class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
    41 {
    42   val options = PIDE.options
    43 
    44   private val predefined =
    45     List(JEdit_Sessions.logic_selector(false), JEdit_Spell_Checker.dictionaries_selector())
    46 
    47   protected val components =
    48     options.make_components(predefined,
    49       (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
    50 }
    51 
    52 
    53 class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
    54 {
    55   private val predefined =
    56     (for {
    57       (name, opt) <- PIDE.options.value.options.toList
    58       if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
    59     } yield PIDE.options.make_color_component(opt))
    60 
    61   assert(predefined.nonEmpty)
    62 
    63   protected val components = PIDE.options.make_components(predefined, _ => false)
    64 }
    65