4 * @author Johannes Hölzl, TU Munich |
4 * @author Johannes Hölzl, TU Munich |
5 */ |
5 */ |
6 |
6 |
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 import java.lang.Integer |
9 import javax.swing.{JComboBox, JSpinner} |
10 |
|
11 import java.awt.BorderLayout |
|
12 import java.awt.GridBagConstraints.HORIZONTAL |
|
13 import java.awt.BorderLayout.{WEST, CENTER, EAST} |
|
14 import java.awt.event.{ActionListener, ActionEvent} |
|
15 import javax.swing.{JTextField, JButton, JPanel, JLabel, JFileChooser, JSpinner, JComboBox} |
|
16 |
10 |
17 import org.gjt.sp.jedit.AbstractOptionPane |
11 import org.gjt.sp.jedit.AbstractOptionPane |
18 |
12 |
19 |
13 |
20 class OptionPane extends AbstractOptionPane("isabelle") { |
14 class OptionPane extends AbstractOptionPane("isabelle") |
21 var pathName = new JTextField() |
15 { |
22 var fontSize = new JSpinner() |
16 private val logic_name = new JComboBox() |
23 var logicName = new JComboBox() |
17 private val font_size = new JSpinner() |
24 |
|
25 override def _init() { |
|
26 addComponent(Isabelle.Property("font-path.title"), { |
|
27 val pickPath = new JButton("...") |
|
28 pickPath.addActionListener(new ActionListener() { |
|
29 override def actionPerformed(e : ActionEvent) { |
|
30 val chooser = new JFileChooser(pathName.getText()) |
|
31 if (chooser.showOpenDialog(OptionPane.this) == JFileChooser.APPROVE_OPTION) |
|
32 pathName.setText(chooser.getSelectedFile().getAbsolutePath()) |
|
33 } |
|
34 }) |
|
35 |
18 |
36 pathName.setText(Isabelle.Property("font-path")) |
19 override def _init() |
37 |
20 { |
38 val pathPanel = new JPanel(new BorderLayout()) |
|
39 pathPanel.add(pathName, CENTER) |
|
40 pathPanel.add(pickPath, EAST) |
|
41 pathPanel |
|
42 }, HORIZONTAL) |
|
43 |
|
44 addComponent(Isabelle.Property("font-size.title"), { |
|
45 try { |
|
46 if (Isabelle.Property("font-size") != null) |
|
47 fontSize.setValue(Isabelle.Property("font-size").toInt) |
|
48 } |
|
49 catch { |
|
50 case e : NumberFormatException => |
|
51 fontSize.setValue(14) |
|
52 } |
|
53 |
|
54 fontSize |
|
55 }) |
|
56 |
|
57 addComponent(Isabelle.Property("logic.title"), { |
21 addComponent(Isabelle.Property("logic.title"), { |
58 for (name <- Isabelle.system.find_logics()) { |
22 for (name <- Isabelle.system.find_logics()) { |
59 logicName.addItem(name) |
23 logic_name.addItem(name) |
60 if (name == Isabelle.Property("logic")) |
24 if (name == Isabelle.Property("logic")) |
61 logicName.setSelectedItem(name) |
25 logic_name.setSelectedItem(name) |
62 } |
26 } |
63 |
27 logic_name |
64 logicName |
28 }) |
|
29 addComponent(Isabelle.Property("font-size.title"), { |
|
30 font_size.setValue(Isabelle.Int_Property("font-size")) |
|
31 font_size |
65 }) |
32 }) |
66 } |
33 } |
67 |
34 |
68 override def _save() { |
35 override def _save() |
69 val size = fontSize.getValue() |
36 { |
70 val name = pathName.getText() |
37 val logic = logic_name.getSelectedItem.asInstanceOf[String] |
71 if (Isabelle.Property("font-path") != name || Isabelle.Property("font-size") != size.toString) { |
38 Isabelle.Property("logic") = logic |
72 Isabelle.Property("font-path") = name |
39 |
73 Isabelle.Property("font-size") = size.toString |
40 val size = font_size.getValue().asInstanceOf[Int] |
74 Swing.later { Isabelle.plugin.set_font(name, size.asInstanceOf[Integer].intValue) } |
41 if (Isabelle.Int_Property("font-size") != size) |
|
42 { |
|
43 Isabelle.Int_Property("font-size") = size |
|
44 Swing.later { Isabelle.plugin.set_font(size) } |
75 } |
45 } |
76 |
|
77 val logic = logicName.getSelectedItem.asInstanceOf[String] |
|
78 Isabelle.Property("logic") = logic |
|
79 } |
46 } |
80 } |
47 } |