src/Tools/jEdit/src/isabelle_options.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73340 0ffcad1f6130
child 75829 b8a4f9b1eed6
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    15
abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    16
  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
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    18
  override def _init(): Unit = {
49271
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    19
    val dummy_property = "options.isabelle.dummy"
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    20
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    21
    for ((s, cs) <- components) {
49271
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    22
      if (s != "") {
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    23
        jEdit.setProperty(dummy_property, s)
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    24
        addSeparator(dummy_property)
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    25
        jEdit.setProperty(dummy_property, null)
b08f9d534a2a need to provide label via some jEdit property;
wenzelm
parents: 49270
diff changeset
    26
      }
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    27
      cs.foreach(c => addComponent(c.title, c.peer))
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    28
    }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    29
  }
34617
8d2c49605685 simplified option pane: proper logic title, hardwired font path;
wenzelm
parents: 34506
diff changeset
    30
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    31
  override def _save(): Unit = {
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49250
diff changeset
    32
    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
    33
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    34
}
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    35
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    36
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    37
class Isabelle_Options1 extends Isabelle_Options("isabelle-general") {
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 66460
diff changeset
    38
  val options: JEdit_Options = PIDE.options
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 52065
diff changeset
    39
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 52065
diff changeset
    40
  private val predefined =
66460
f7b0d6fb417a proper update of options (amending c3d6dd17d626);
wenzelm
parents: 65256
diff changeset
    41
    List(JEdit_Sessions.logic_selector(options, false),
65256
c3d6dd17d626 more explicit options;
wenzelm
parents: 65139
diff changeset
    42
      JEdit_Spell_Checker.dictionaries_selector())
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 52065
diff changeset
    43
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    44
  protected val components =
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 52065
diff changeset
    45
    options.make_components(predefined,
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51554
diff changeset
    46
      (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
49354
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73340
diff changeset
    50
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") {
49354
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
59319
wenzelm
parents: 56559
diff changeset
    57
  assert(predefined.nonEmpty)
49354
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