19 import org.gjt.sp.jedit.{jEdit, View} |
19 import org.gjt.sp.jedit.{jEdit, View} |
20 import org.gjt.sp.util.GenericGUIUtilities |
20 import org.gjt.sp.util.GenericGUIUtilities |
21 import org.jedit.keymap.{KeymapManager, Keymap} |
21 import org.jedit.keymap.{KeymapManager, Keymap} |
22 |
22 |
23 |
23 |
24 object Keymap_Merge |
24 object Keymap_Merge { |
25 { |
|
26 /** shortcuts **/ |
25 /** shortcuts **/ |
27 |
26 |
28 private def is_shortcut(property: String): Boolean = |
27 private def is_shortcut(property: String): Boolean = |
29 (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && |
28 (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && |
30 !property.startsWith("options.shortcuts.") |
29 !property.startsWith("options.shortcuts.") |
31 |
30 |
32 class Shortcut(val property: String, val binding: String) |
31 class Shortcut(val property: String, val binding: String) { |
33 { |
|
34 override def toString: String = Properties.Eq(property, binding) |
32 override def toString: String = Properties.Eq(property, binding) |
35 |
33 |
36 def primary: Boolean = property.endsWith(".shortcut") |
34 def primary: Boolean = property.endsWith(".shortcut") |
37 |
35 |
38 val action: String = |
36 val action: String = |
77 } |
75 } |
78 } |
76 } |
79 result.sortBy(_.property) |
77 result.sortBy(_.property) |
80 } |
78 } |
81 |
79 |
82 def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] = |
80 def get_shortcut_conflicts( |
83 { |
81 keymap_name: String, |
|
82 keymap: Keymap |
|
83 ): List[(Shortcut, List[Shortcut])] = { |
84 val keymap_shortcuts = |
84 val keymap_shortcuts = |
85 if (keymap == null) Nil |
85 if (keymap == null) Nil |
86 else convert_properties(Untyped.get[JProperties](keymap, "props")) |
86 else convert_properties(Untyped.get[JProperties](keymap, "props")) |
87 |
87 |
88 for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield { |
88 for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield { |
99 /** table **/ |
99 /** table **/ |
100 |
100 |
101 private def conflict_color: Color = |
101 private def conflict_color: Color = |
102 PIDE.options.color_value("error_color") |
102 PIDE.options.color_value("error_color") |
103 |
103 |
104 private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) |
104 private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) { |
105 { |
|
106 override def toString: String = |
105 override def toString: String = |
107 if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" |
106 if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" |
108 else |
107 else |
109 "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" + |
108 "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" + |
110 HTML.output("--- " + shortcut.toString) + |
109 HTML.output("--- " + shortcut.toString) + |
111 "</font></html>" |
110 "</font></html>" |
112 } |
111 } |
113 |
112 |
114 private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel |
113 private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel { |
115 { |
|
116 private val entries_count = entries.length |
114 private val entries_count = entries.length |
117 private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count |
115 private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count |
118 private def get_entry(row: Int): Option[Table_Entry] = |
116 private def get_entry(row: Int): Option[Table_Entry] = |
119 if (has_entry(row)) Some(entries(row)) else None |
117 if (has_entry(row)) Some(entries(row)) else None |
120 |
118 |
126 selected.value.contains(row) |
124 selected.value.contains(row) |
127 |
125 |
128 private def select(head: Int, tail: List[Int], b: Boolean): Unit = |
126 private def select(head: Int, tail: List[Int], b: Boolean): Unit = |
129 selected.change(set => if (b) set + head -- tail else set - head ++ tail) |
127 selected.change(set => if (b) set + head -- tail else set - head ++ tail) |
130 |
128 |
131 def apply(keymap_name: String, keymap: Keymap): Unit = |
129 def apply(keymap_name: String, keymap: Keymap): Unit = { |
132 { |
|
133 GUI_Thread.require {} |
130 GUI_Thread.require {} |
134 |
131 |
135 for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { |
132 for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { |
136 val b = is_selected(row) |
133 val b = is_selected(row) |
137 if (b) { |
134 if (b) { |
151 override def getColumnName(i: Int): String = |
148 override def getColumnName(i: Int): String = |
152 if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" |
149 if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" |
153 |
150 |
154 override def getRowCount: Int = entries_count |
151 override def getRowCount: Int = entries_count |
155 |
152 |
156 override def getValueAt(row: Int, column: Int): AnyRef = |
153 override def getValueAt(row: Int, column: Int): AnyRef = { |
157 { |
|
158 get_entry(row) match { |
154 get_entry(row) match { |
159 case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row)) |
155 case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row)) |
160 case Some(entry) if column == 1 => entry |
156 case Some(entry) if column == 1 => entry |
161 case _ => null |
157 case _ => null |
162 } |
158 } |
163 } |
159 } |
164 |
160 |
165 override def isCellEditable(row: Int, column: Int): Boolean = |
161 override def isCellEditable(row: Int, column: Int): Boolean = |
166 has_entry(row) && column == 0 |
162 has_entry(row) && column == 0 |
167 |
163 |
168 override def setValueAt(value: AnyRef, row: Int, column: Int): Unit = |
164 override def setValueAt(value: AnyRef, row: Int, column: Int): Unit = { |
169 { |
|
170 value match { |
165 value match { |
171 case obj: java.lang.Boolean if has_entry(row) && column == 0 => |
166 case obj: java.lang.Boolean if has_entry(row) && column == 0 => |
172 val b = obj.booleanValue |
167 val b = obj.booleanValue |
173 val entry = entries(row) |
168 val entry = entries(row) |
174 entry.head match { |
169 entry.head match { |
181 case _ => |
176 case _ => |
182 } |
177 } |
183 } |
178 } |
184 } |
179 } |
185 |
180 |
186 private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) |
181 private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) { |
187 { |
|
188 private val cell_size = GenericGUIUtilities.defaultTableCellSize() |
182 private val cell_size = GenericGUIUtilities.defaultTableCellSize() |
189 private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) |
183 private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) |
190 |
184 |
191 val table = new JTable(table_model) |
185 val table = new JTable(table_model) |
192 table.setShowGrid(false) |
186 table.setShowGrid(false) |
211 |
205 |
212 |
206 |
213 |
207 |
214 /** check with optional dialog **/ |
208 /** check with optional dialog **/ |
215 |
209 |
216 def check_dialog(view: View): Unit = |
210 def check_dialog(view: View): Unit = { |
217 { |
|
218 GUI_Thread.require {} |
211 GUI_Thread.require {} |
219 |
212 |
220 val keymap_manager = jEdit.getKeymapManager |
213 val keymap_manager = jEdit.getKeymapManager |
221 val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) |
214 val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) |
222 val keymap = |
215 val keymap = |
246 JOptionPane.OK_CANCEL_OPTION, |
239 JOptionPane.OK_CANCEL_OPTION, |
247 "The following Isabelle keymap changes are in conflict with the current", |
240 "The following Isabelle keymap changes are in conflict with the current", |
248 "jEdit keymap " + quote(keymap_name) + ":", |
241 "jEdit keymap " + quote(keymap_name) + ":", |
249 new Table(table_model), |
242 new Table(table_model), |
250 "Selected shortcuts will be applied, unselected changes will be ignored.", |
243 "Selected shortcuts will be applied, unselected changes will be ignored.", |
251 "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0) |
244 "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0) { |
252 { table_model.apply(keymap_name, keymap) } |
245 table_model.apply(keymap_name, keymap) |
|
246 } |
253 |
247 |
254 no_shortcut_conflicts.foreach(_.set(keymap)) |
248 no_shortcut_conflicts.foreach(_.set(keymap)) |
255 |
249 |
256 keymap.save() |
250 keymap.save() |
257 jEdit.saveSettings() |
251 jEdit.saveSettings() |