src/Tools/jEdit/src/isabelle_options.scala
author wenzelm
Sat, 25 May 2013 17:40:44 +0200
changeset 52147 9943f8067f11
parent 52065 78f2475aa126
child 56559 eece73c31e38
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 40850
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_options.scala
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents: 49245
diff changeset
     2
    Author:     Makarius
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 34782
diff changeset
     3
b82a698ef6c9 tuned headers;
wenzelm
parents: 34782
diff changeset
     4
Editor pane for plugin options.
b82a698ef6c9 tuned headers;
wenzelm
parents: 34782
diff changeset
     5
*/
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34318
diff changeset
     6
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     8
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
     9
40850
d804de9ac970 more abstract handling of Time properties;
wenzelm
parents: 40849
diff changeset
    10
import isabelle._
d804de9ac970 more abstract handling of Time properties;
wenzelm
parents: 40849
diff changeset
    11
49271
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    12
import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    13
34468
9d4b4f290676 maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents: 34441
diff changeset
    14
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    15
abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name)
34617
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    16
{
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    17
  protected val components: List[(String, List[Option_Component])]
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    18
34617
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    19
  override def _init()
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    20
  {
49271
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    21
    val dummy_property = "options.isabelle.dummy"
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    22
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    23
    for ((s, cs) <- components) {
49271
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    24
      if (s != "") {
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    25
        jEdit.setProperty(dummy_property, s)
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    26
        addSeparator(dummy_property)
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    27
        jEdit.setProperty(dummy_property, null)
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    28
      }
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    29
      cs.foreach(c => addComponent(c.title, c.peer))
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    30
    }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    31
  }
34617
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    32
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    33
  override def _save()
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    34
  {
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    35
    for ((_, cs) <- components) cs.foreach(_.save())
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    36
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    37
}
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    38
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    39
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    40
class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    41
{
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51554
diff changeset
    42
  val options = PIDE.options
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    43
  protected val components =
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51554
diff changeset
    44
    options.make_components(List(Isabelle_Logic.logic_selector(false)),
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51554
diff changeset
    45
      (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    46
}
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    47
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    48
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    49
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    50
{
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    51
  private val predefined =
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    52
    (for {
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    53
      (name, opt) <- PIDE.options.value.options.toList
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51554
diff changeset
    54
      if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    55
    } yield PIDE.options.make_color_component(opt))
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    56
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    57
  assert(!predefined.isEmpty)
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    58
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    59
  protected val components = PIDE.options.make_components(predefined, _ => false)
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    60
}
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    61