author | wenzelm |
Mon, 31 May 2010 09:47:41 +0200 | |
changeset 37203 | c4261f3bbdd7 |
parent 37201 | 8517a650cfdc |
child 38854 | eb6a35be18ca |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/isabelle_options.scala |
2 |
Author: Johannes Hölzl, TU Munich |
|
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 |
|
34617
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
10 |
import javax.swing.{JComboBox, JSpinner} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
import org.gjt.sp.jedit.AbstractOptionPane |
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 |
|
34760 | 15 |
class Isabelle_Options extends AbstractOptionPane("isabelle") |
34617
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
16 |
{ |
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
17 |
private val logic_name = new JComboBox() |
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
18 |
private val relative_font_size = new JSpinner() |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
19 |
private val tooltip_font_size = new JSpinner() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
|
34782
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
21 |
private class List_Item(val name: String, val descr: String) { |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
22 |
def this(name: String) = this(name, name) |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
23 |
override def toString = descr |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
24 |
} |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
25 |
|
34617
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
26 |
override def _init() |
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
27 |
{ |
34781 | 28 |
val logic = Isabelle.Property("logic") |
34468
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34441
diff
changeset
|
29 |
addComponent(Isabelle.Property("logic.title"), { |
34782
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
30 |
logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")")) |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
31 |
for (name <- Isabelle.system.find_logics()) { |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
32 |
val item = new List_Item(name) |
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
33 |
logic_name.addItem(item) |
34781 | 34 |
if (name == logic) |
34782
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
35 |
logic_name.setSelectedItem(item) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
36 |
} |
34617
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
37 |
logic_name |
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
38 |
}) |
34782
fcd6a41326a6
refined treatment of default logic concerning property and GUI;
wenzelm
parents:
34781
diff
changeset
|
39 |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
40 |
addComponent(Isabelle.Property("relative-font-size.title"), { |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
41 |
relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100)) |
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
42 |
relative_font_size |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
43 |
}) |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
44 |
|
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
45 |
addComponent(Isabelle.Property("tooltip-font-size.title"), { |
37203
c4261f3bbdd7
more flexibile font size via CSS <style> instead of old <font> element;
wenzelm
parents:
37201
diff
changeset
|
46 |
tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10)) |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
47 |
tooltip_font_size |
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
48 |
}) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
49 |
} |
34617
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
50 |
|
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
51 |
override def _save() |
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
52 |
{ |
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
53 |
Isabelle.Property("logic") = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
54 |
logic_name.getSelectedItem.asInstanceOf[List_Item].name |
34617
8d2c49605685
simplified option pane: proper logic title, hardwired font path;
wenzelm
parents:
34506
diff
changeset
|
55 |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
56 |
Isabelle.Int_Property("relative-font-size") = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
57 |
relative_font_size.getValue().asInstanceOf[Int] |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
58 |
|
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
59 |
Isabelle.Int_Property("tooltip-font-size") = |
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
36817
diff
changeset
|
60 |
tooltip_font_size.getValue().asInstanceOf[Int] |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
61 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
62 |
} |