src/Tools/jEdit/src/isabelle_options.scala
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 51533 3f6280aedbcc
child 51554 041bc3d31f23
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
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 =
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51071
diff changeset
    44
    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
51441
37f699750430 more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm
parents: 51423
diff changeset
    45
      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51441
diff changeset
    46
      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51533
diff changeset
    47
      "jedit_timing_threshold", "skip_proofs", "threads", "threads_trace", "parallel_proofs",
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51441
diff changeset
    48
      "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51441
diff changeset
    49
      "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51441
diff changeset
    50
      "editor_update_delay", "editor_chart_delay")
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    51
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    52
  relevant_options.foreach(PIDE.options.value.check_name _)
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    53
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    54
  protected val components =
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    55
    PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    56
}
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    57
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    58
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    59
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    60
{
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    61
  // FIXME avoid hard-wired stuff
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    62
  private val predefined =
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    63
    (for {
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    64
      (name, opt) <- PIDE.options.value.options.toList
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49354
diff changeset
    65
      if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    66
    } yield PIDE.options.make_color_component(opt))
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    67
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    68
  assert(!predefined.isEmpty)
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    69
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50190
diff changeset
    70
  protected val components = PIDE.options.make_components(predefined, _ => false)
49354
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    71
}
65c6a1d62dbc more scalable option-group;
wenzelm
parents: 49296
diff changeset
    72