|
1 /* Title: Tools/jEdit/src/isabelle_options.scala |
|
2 Author: Johannes Hölzl, TU Munich |
|
3 |
|
4 Editor pane for plugin options. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import javax.swing.JSpinner |
|
13 |
|
14 import scala.swing.CheckBox |
|
15 |
|
16 import org.gjt.sp.jedit.AbstractOptionPane |
|
17 |
|
18 |
|
19 class Isabelle_Options extends AbstractOptionPane("isabelle") |
|
20 { |
|
21 private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic")) |
|
22 private val auto_start = new CheckBox() |
|
23 private val relative_font_size = new JSpinner() |
|
24 private val tooltip_font_size = new JSpinner() |
|
25 private val tooltip_margin = new JSpinner() |
|
26 private val tooltip_dismiss_delay = new JSpinner() |
|
27 |
|
28 override def _init() |
|
29 { |
|
30 addComponent(Isabelle.Property("logic.title"), logic_selector.peer) |
|
31 |
|
32 addComponent(Isabelle.Property("auto-start.title"), auto_start.peer) |
|
33 auto_start.selected = Isabelle.Boolean_Property("auto-start") |
|
34 |
|
35 relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100)) |
|
36 addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size) |
|
37 |
|
38 tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10)) |
|
39 addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size) |
|
40 |
|
41 tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40)) |
|
42 addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin) |
|
43 |
|
44 tooltip_dismiss_delay.setValue( |
|
45 Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt) |
|
46 addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay) |
|
47 } |
|
48 |
|
49 override def _save() |
|
50 { |
|
51 Isabelle.Property("logic") = logic_selector.selection.item.name |
|
52 |
|
53 Isabelle.Boolean_Property("auto-start") = auto_start.selected |
|
54 |
|
55 Isabelle.Int_Property("relative-font-size") = |
|
56 relative_font_size.getValue().asInstanceOf[Int] |
|
57 |
|
58 Isabelle.Int_Property("tooltip-font-size") = |
|
59 tooltip_font_size.getValue().asInstanceOf[Int] |
|
60 |
|
61 Isabelle.Int_Property("tooltip-margin") = |
|
62 tooltip_margin.getValue().asInstanceOf[Int] |
|
63 |
|
64 Isabelle.Time_Property("tooltip-dismiss-delay") = |
|
65 Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int]) |
|
66 } |
|
67 } |