author | wenzelm |
Fri, 12 Aug 2022 12:50:19 +0200 | |
changeset 75816 | 91f02f224b80 |
parent 75393 | 87ebf5a50283 |
child 75829 | b8a4f9b1eed6 |
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 |
|
75393 | 15 |
abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) { |
49354 | 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 | 18 |
override def _init(): Unit = { |
49271 | 19 |
val dummy_property = "options.isabelle.dummy" |
20 |
||
49270 | 21 |
for ((s, cs) <- components) { |
49271 | 22 |
if (s != "") { |
23 |
jEdit.setProperty(dummy_property, s) |
|
24 |
addSeparator(dummy_property) |
|
25 |
jEdit.setProperty(dummy_property, null) |
|
26 |
} |
|
49270 | 27 |
cs.foreach(c => addComponent(c.title, c.peer)) |
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 | 31 |
override def _save(): Unit = { |
49270 | 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 | 35 |
|
36 |
||
75393 | 37 |
class Isabelle_Options1 extends Isabelle_Options("isabelle-general") { |
71601 | 38 |
val options: JEdit_Options = PIDE.options |
56559 | 39 |
|
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 | 42 |
JEdit_Spell_Checker.dictionaries_selector()) |
56559 | 43 |
|
49354 | 44 |
protected val components = |
56559 | 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 | 47 |
} |
48 |
||
49 |
||
75393 | 50 |
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") { |
49354 | 51 |
private val predefined = |
52 |
(for { |
|
50205 | 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 | 55 |
} yield PIDE.options.make_color_component(opt)) |
49354 | 56 |
|
59319 | 57 |
assert(predefined.nonEmpty) |
49354 | 58 |
|
50205 | 59 |
protected val components = PIDE.options.make_components(predefined, _ => false) |
49354 | 60 |
} |
61 |