src/Tools/jEdit/src/isabelle_options.scala
author wenzelm
Sun, 18 Nov 2012 16:04:13 +0100
changeset 50119 5c370a036de7
parent 50117 32755e357a51
child 50190 0d7f0d8fd63b
permissions -rw-r--r--
more generous tracing_limit, with explicit system option;
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
{
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    42
  // FIXME avoid hard-wired stuff
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    43
  private val relevant_options =
49969
72216713733a further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents: 49722
diff changeset
    44
    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
50117
32755e357a51 update options via protocol;
wenzelm
parents: 49969
diff changeset
    45
      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "threads", "threads_trace",
32755e357a51 update options via protocol;
wenzelm
parents: 49969
diff changeset
    46
      "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay",
50119
5c370a036de7 more generous tracing_limit, with explicit system option;
wenzelm
parents: 50117
diff changeset
    47
      "editor_input_delay", "editor_output_delay", "editor_reparse_limit", "editor_tracing_limit",
5c370a036de7 more generous tracing_limit, with explicit system option;
wenzelm
parents: 50117
diff changeset
    48
      "editor_update_delay")
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    49
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    50
  relevant_options.foreach(Isabelle.options.value.check_name _)
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    51
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    52
  protected val components =
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    53
    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    54
}
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    55
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    56
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    57
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    58
{
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    59
  // FIXME avoid hard-wired stuff
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    60
  private val predefined =
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    61
    (for {
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    62
      (name, opt) <- Isabelle.options.value.options.toList
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49354
diff changeset
    63
      if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    64
    } yield Isabelle.options.make_color_component(opt))
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    65
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    66
  assert(!predefined.isEmpty)
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    67
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    68
  protected val components = Isabelle.options.make_components(predefined, _ => false)
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    69
}
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    70