author | wenzelm |
Thu, 31 Jan 2013 22:21:05 +0100 | |
changeset 51071 | b7e7557e80b5 |
parent 50698 | 49621c755075 |
child 51423 | e5f9a6d9ca82 |
permissions | -rw-r--r-- |
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 | 2 |
Author: Makarius |
36760 | 3 |
|
4 |
Editor pane for plugin options. |
|
5 |
*/ |
|
34407 | 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 | 9 |
|
40850 | 10 |
import isabelle._ |
11 |
||
49271 | 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 | 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 | 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 | 21 |
val dummy_property = "options.isabelle.dummy" |
22 |
||
49270 | 23 |
for ((s, cs) <- components) { |
49271 | 24 |
if (s != "") { |
25 |
jEdit.setProperty(dummy_property, s) |
|
26 |
addSeparator(dummy_property) |
|
27 |
jEdit.setProperty(dummy_property, null) |
|
28 |
} |
|
49270 | 29 |
cs.foreach(c => addComponent(c.title, c.peer)) |
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 | 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 | 38 |
|
39 |
||
40 |
class Isabelle_Options1 extends Isabelle_Options("isabelle-general") |
|
41 |
{ |
|
42 |
// FIXME avoid hard-wired stuff |
|
43 |
private val relevant_options = |
|
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50505
diff
changeset
|
44 |
Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit", |
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50505
diff
changeset
|
45 |
"jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin", |
51071
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50698
diff
changeset
|
46 |
"jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs", |
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50698
diff
changeset
|
47 |
"parallel_proofs_threshold", "editor_load_delay", "editor_input_delay", |
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50698
diff
changeset
|
48 |
"editor_output_delay", "editor_reparse_limit", "editor_tracing_messages", |
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50698
diff
changeset
|
49 |
"editor_update_delay", "editor_chart_delay") |
49354 | 50 |
|
50205 | 51 |
relevant_options.foreach(PIDE.options.value.check_name _) |
49354 | 52 |
|
53 |
protected val components = |
|
50205 | 54 |
PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options) |
49354 | 55 |
} |
56 |
||
57 |
||
58 |
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") |
|
59 |
{ |
|
60 |
// FIXME avoid hard-wired stuff |
|
61 |
private val predefined = |
|
62 |
(for { |
|
50205 | 63 |
(name, opt) <- PIDE.options.value.options.toList |
49355 | 64 |
if (name.endsWith("_color") && opt.section == "Rendering of Document Content") |
50205 | 65 |
} yield PIDE.options.make_color_component(opt)) |
49354 | 66 |
|
67 |
assert(!predefined.isEmpty) |
|
68 |
||
50205 | 69 |
protected val components = PIDE.options.make_components(predefined, _ => false) |
49354 | 70 |
} |
71 |