|
1 /* Title: Tools/jEdit/src/keymap_merge.scala |
|
2 Author: Makarius |
|
3 |
|
4 Merge of Isabelle/jEdit shortcuts wrt. jEdit keymap. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.awt.event.WindowEvent |
|
13 import javax.swing.{WindowConstants, JDialog, JTable, JScrollPane} |
|
14 |
|
15 import scala.collection.mutable |
|
16 import scala.collection.JavaConversions |
|
17 import scala.collection.immutable.SortedSet |
|
18 import scala.swing.{FlowPanel, BorderPanel, Component, Button} |
|
19 import scala.swing.event.ButtonClicked |
|
20 |
|
21 import org.gjt.sp.jedit.{jEdit, View, GUIUtilities} |
|
22 import org.jedit.keymap.{KeymapManager, Keymap} |
|
23 |
|
24 |
|
25 object Keymap_Merge |
|
26 { |
|
27 /* Isabelle/jEdit shortcuts */ |
|
28 |
|
29 sealed case class Shortcut(action: String, key: String, alternative: Boolean) |
|
30 { |
|
31 def eq_action(that: Shortcut): Boolean = action == that.action |
|
32 |
|
33 val property: String = if (alternative) action + ".shortcut2" else action + ".shortcut" |
|
34 val label: String = |
|
35 GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) |
|
36 } |
|
37 |
|
38 def additional_shortcuts(): List[Shortcut] = |
|
39 { |
|
40 val result = new mutable.ListBuffer[Shortcut] |
|
41 for (entry <- JavaConversions.mapAsScalaMap(jEdit.getProperties)) { |
|
42 entry match { |
|
43 case (a: String, b: String) if a.endsWith(".shortcut") => |
|
44 val action = a.substring(0, a.length - 9) |
|
45 result += Shortcut(action, b, false) |
|
46 case (a: String, b: String) if a.endsWith(".shortcut2") => |
|
47 val action = a.substring(0, a.length - 10) |
|
48 result += Shortcut(action, b, true) |
|
49 case _ => |
|
50 } |
|
51 } |
|
52 result.toList |
|
53 } |
|
54 |
|
55 |
|
56 /* jEdit keymap */ |
|
57 |
|
58 def current_keymap(): Keymap = |
|
59 { |
|
60 val manager = jEdit.getKeymapManager |
|
61 val name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) |
|
62 manager.getKeymap(name) match { |
|
63 case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) |
|
64 case keymap => keymap |
|
65 } |
|
66 } |
|
67 |
|
68 |
|
69 |
|
70 /** dialog **/ |
|
71 |
|
72 def dialog(view: View) |
|
73 { |
|
74 GUI_Thread.require {} |
|
75 new Dialog(view) |
|
76 } |
|
77 |
|
78 private class Dialog(view: View) extends JDialog(view) |
|
79 { |
|
80 /* table */ |
|
81 |
|
82 val shortcuts = additional_shortcuts() |
|
83 |
|
84 def get_label(action: String): String = |
|
85 shortcuts.collectFirst( |
|
86 { case s if s.action == action && s.label != "" => s.label }).getOrElse(action) |
|
87 |
|
88 def get_key(action: String, alternative: Boolean): String = |
|
89 shortcuts.collectFirst( |
|
90 { case s if s.action == action && s.alternative == alternative => s.key }).getOrElse("") |
|
91 |
|
92 val column_names: Array[AnyRef] = |
|
93 Array(jEdit.getProperty("options.shortcuts.name"), |
|
94 jEdit.getProperty("options.shortcuts.shortcut1"), |
|
95 jEdit.getProperty("options.shortcuts.shortcut2")) |
|
96 |
|
97 val table_rows: Array[Array[AnyRef]] = |
|
98 Library.distinct[Shortcut](shortcuts, _ eq_action _).sortBy(_.action). |
|
99 map(s => Array[AnyRef](s.label, get_key(s.action, false), get_key(s.action, true))).toArray |
|
100 |
|
101 val table = new JTable(table_rows, column_names) |
|
102 table.setRowHeight(GUIUtilities.defaultRowHeight()) |
|
103 table.getTableHeader().setReorderingAllowed(false) // FIXME !? |
|
104 |
|
105 val table_size = table.getPreferredSize() |
|
106 table_size.height = table_size.height min 200 |
|
107 |
|
108 val table_scroller = new JScrollPane(table) |
|
109 table_scroller.setPreferredSize(table_size) |
|
110 |
|
111 |
|
112 /* buttons */ |
|
113 |
|
114 val ok_button = new Button("OK") { |
|
115 reactions += { case ButtonClicked(_) => close() } // FIXME |
|
116 } |
|
117 |
|
118 val cancel_button = new Button("Cancel") { |
|
119 reactions += { case ButtonClicked(_) => close() } // FIXME |
|
120 } |
|
121 |
|
122 private def close() |
|
123 { |
|
124 setVisible(false) |
|
125 dispose() |
|
126 } |
|
127 |
|
128 |
|
129 /* layout */ |
|
130 |
|
131 private val action_panel = new FlowPanel(FlowPanel.Alignment.Right)(ok_button, cancel_button) |
|
132 private val layout_panel = new BorderPanel |
|
133 layout_panel.layout(Component.wrap(table_scroller)) = BorderPanel.Position.Center |
|
134 layout_panel.layout(action_panel) = BorderPanel.Position.South |
|
135 |
|
136 setContentPane(layout_panel.peer) |
|
137 |
|
138 |
|
139 /* main */ |
|
140 |
|
141 setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE) |
|
142 |
|
143 setTitle("Isabelle/jEdit keymap changes") |
|
144 |
|
145 pack() |
|
146 setLocationRelativeTo(view) |
|
147 setVisible(true) |
|
148 } |
|
149 } |