| author | wenzelm |
| Mon, 25 Nov 2019 12:16:26 +0100 | |
| changeset 71162 | 4b3e1b859a22 |
| parent 67648 | f6e351043014 |
| child 71359 | 411c0322c09d |
| permissions | -rw-r--r-- |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/keymap_merge.scala |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
3 |
|
| 63736 | 4 |
Merge of Isabelle shortcuts vs. jEdit keymap. |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
6 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
8 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
9 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
11 |
|
| 71162 | 12 |
import java.lang.Class |
| 63745 | 13 |
import java.awt.{Color, Dimension, BorderLayout}
|
14 |
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
|
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
15 |
import javax.swing.table.AbstractTableModel |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
16 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
17 |
import scala.collection.JavaConversions |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
18 |
|
| 63748 | 19 |
import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
20 |
import org.jedit.keymap.{KeymapManager, Keymap}
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
21 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
22 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
23 |
object Keymap_Merge |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
24 |
{
|
| 63736 | 25 |
/** shortcuts **/ |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
26 |
|
| 63736 | 27 |
private def is_shortcut(property: String): Boolean = |
28 |
(property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
|
|
29 |
!property.startsWith("options.shortcuts.")
|
|
30 |
||
31 |
class Shortcut(val property: String, val binding: String) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
32 |
{
|
| 63736 | 33 |
override def toString: String = property + "=" + binding |
34 |
||
35 |
def primary: Boolean = property.endsWith(".shortcut")
|
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
36 |
|
| 63736 | 37 |
val action: String = |
38 |
Library.try_unsuffix(".shortcut", property) orElse
|
|
39 |
Library.try_unsuffix(".shortcut2", property) getOrElse
|
|
40 |
error("Bad shortcut property: " + quote(property))
|
|
41 |
||
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
42 |
val label: String = |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
43 |
GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) |
| 63736 | 44 |
|
45 |
||
| 63745 | 46 |
/* ignore wrt. keymap */ |
| 63736 | 47 |
|
48 |
private def prop_ignore: String = property + ".ignore" |
|
49 |
||
50 |
def ignored_keymaps(): List[String] = |
|
| 66923 | 51 |
space_explode(',', jEdit.getProperty(prop_ignore, ""))
|
| 63736 | 52 |
|
53 |
def is_ignored(keymap_name: String): Boolean = |
|
54 |
ignored_keymaps().contains(keymap_name) |
|
55 |
||
| 63772 | 56 |
def ignore(keymap_name: String): Unit = |
57 |
jEdit.setProperty(prop_ignore, |
|
58 |
Library.insert(keymap_name)(ignored_keymaps()).sorted.mkString(","))
|
|
| 63745 | 59 |
|
60 |
def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding) |
|
61 |
def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
62 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
63 |
|
| 63745 | 64 |
|
65 |
/* content wrt. keymap */ |
|
66 |
||
| 63736 | 67 |
def convert_properties(props: java.util.Properties): List[Shortcut] = |
68 |
if (props == null) Nil |
|
69 |
else {
|
|
70 |
var result = List.empty[Shortcut] |
|
71 |
for (entry <- JavaConversions.mapAsScalaMap(props)) {
|
|
72 |
entry match {
|
|
73 |
case (a: String, b: String) if is_shortcut(a) => |
|
74 |
result ::= new Shortcut(a, b) |
|
75 |
case _ => |
|
76 |
} |
|
77 |
} |
|
78 |
result.sortBy(_.property) |
|
79 |
} |
|
80 |
||
| 63745 | 81 |
def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] = |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
82 |
{
|
| 63736 | 83 |
val keymap_shortcuts = |
84 |
if (keymap == null) Nil |
|
85 |
else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) |
|
86 |
||
| 63745 | 87 |
for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
|
| 63736 | 88 |
val conflicts = |
89 |
keymap_shortcuts.filter(s1 => |
|
90 |
s.property == s1.property && s.binding != s1.binding || |
|
| 63742 | 91 |
s.property != s1.property && s.binding == s1.binding && s1.binding != "") |
| 63736 | 92 |
(s, conflicts) |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
93 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
94 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
95 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
96 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
97 |
|
| 63745 | 98 |
/** table **/ |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
99 |
|
| 63739 | 100 |
private def conflict_color: Color = |
101 |
PIDE.options.color_value("error_color")
|
|
102 |
||
| 63740 | 103 |
private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
104 |
{
|
| 63738 | 105 |
override def toString: String = |
| 63740 | 106 |
if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" |
| 63738 | 107 |
else |
| 63739 | 108 |
"<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" + |
109 |
HTML.output("--- " + shortcut.toString) +
|
|
| 63738 | 110 |
"</font></html>" |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
111 |
} |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
112 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
113 |
private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
114 |
{
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
115 |
private val entries_count = entries.length |
| 63743 | 116 |
private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
117 |
private def get_entry(row: Int): Option[Table_Entry] = |
| 63743 | 118 |
if (has_entry(row)) Some(entries(row)) else None |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
119 |
|
| 63740 | 120 |
private val selected = |
121 |
Synchronized[Set[Int]]( |
|
122 |
(for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet) |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
123 |
|
| 63745 | 124 |
private def is_selected(row: Int): Boolean = |
125 |
selected.value.contains(row) |
|
| 63744 | 126 |
|
| 63745 | 127 |
private def select(head: Int, tail: List[Int], b: Boolean): Unit = |
| 63743 | 128 |
selected.change(set => if (b) set + head -- tail else set - head ++ tail) |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
129 |
|
| 63744 | 130 |
def apply(keymap_name: String, keymap: Keymap) |
131 |
{
|
|
132 |
GUI_Thread.require {}
|
|
133 |
||
134 |
for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
|
|
135 |
val b = is_selected(row) |
|
136 |
if (b) {
|
|
| 63745 | 137 |
entry.tail.foreach(i => entries(i).shortcut.reset(keymap)) |
138 |
entry.shortcut.set(keymap) |
|
| 63744 | 139 |
} |
| 63750 | 140 |
else |
141 |
entry.shortcut.ignore(keymap_name) |
|
| 63744 | 142 |
} |
143 |
} |
|
144 |
||
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
145 |
override def getColumnCount: Int = 2 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
146 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
147 |
override def getColumnClass(i: Int): Class[_ <: Object] = |
| 71162 | 148 |
if (i == 0) classOf[java.lang.Boolean] else classOf[Object] |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
149 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
150 |
override def getColumnName(i: Int): String = |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
151 |
if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
152 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
153 |
override def getRowCount: Int = entries_count |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
154 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
155 |
override def getValueAt(row: Int, column: Int): AnyRef = |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
156 |
{
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
157 |
get_entry(row) match {
|
| 71162 | 158 |
case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row)) |
| 63738 | 159 |
case Some(entry) if column == 1 => entry |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
160 |
case _ => null |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
161 |
} |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
162 |
} |
| 63739 | 163 |
|
164 |
override def isCellEditable(row: Int, column: Int): Boolean = |
|
| 63743 | 165 |
has_entry(row) && column == 0 |
| 63739 | 166 |
|
167 |
override def setValueAt(value: AnyRef, row: Int, column: Int) |
|
168 |
{
|
|
| 63743 | 169 |
value match {
|
| 71162 | 170 |
case obj: java.lang.Boolean if has_entry(row) && column == 0 => |
| 63740 | 171 |
val b = obj.booleanValue |
| 63743 | 172 |
val entry = entries(row) |
173 |
entry.head match {
|
|
174 |
case None => select(row, entry.tail, b) |
|
175 |
case Some(head_row) => |
|
176 |
val head_entry = entries(head_row) |
|
177 |
select(head_row, head_entry.tail, !b) |
|
| 63740 | 178 |
} |
| 63743 | 179 |
GUI_Thread.later { fireTableDataChanged() }
|
| 63739 | 180 |
case _ => |
181 |
} |
|
182 |
} |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
183 |
} |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
184 |
|
| 63745 | 185 |
private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
186 |
{
|
| 63745 | 187 |
private val cell_size = GUIUtilities.defaultTableCellSize() |
188 |
private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) |
|
| 63741 | 189 |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
190 |
val table = new JTable(table_model) |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
191 |
table.setShowGrid(false) |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
192 |
table.setIntercellSpacing(new Dimension(0, 0)) |
| 63741 | 193 |
table.setRowHeight(cell_size.height + 2) |
194 |
table.setPreferredScrollableViewportSize(table_size) |
|
195 |
table.setFillsViewportHeight(true) |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
196 |
table.getTableHeader.setReorderingAllowed(false) |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
197 |
|
| 63745 | 198 |
table.getColumnModel.getColumn(0).setPreferredWidth(30) |
199 |
table.getColumnModel.getColumn(0).setMinWidth(30) |
|
200 |
table.getColumnModel.getColumn(0).setMaxWidth(30) |
|
201 |
table.getColumnModel.getColumn(0).setResizable(false) |
|
202 |
table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
203 |
|
| 63745 | 204 |
val scroller = new JScrollPane(table) |
205 |
scroller.getViewport.setBackground(table.getBackground) |
|
206 |
scroller.setPreferredSize(table_size) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
207 |
|
| 63745 | 208 |
add(scroller, BorderLayout.CENTER) |
209 |
} |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
210 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
211 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
212 |
|
| 63745 | 213 |
/** check with optional dialog **/ |
214 |
||
| 63748 | 215 |
def check_dialog(view: View) |
| 63745 | 216 |
{
|
217 |
GUI_Thread.require {}
|
|
218 |
||
219 |
val keymap_manager = jEdit.getKeymapManager |
|
220 |
val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
|
|
221 |
val keymap = |
|
222 |
keymap_manager.getKeymap(keymap_name) match {
|
|
223 |
case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) |
|
224 |
case keymap => keymap |
|
225 |
} |
|
226 |
||
227 |
val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap) |
|
228 |
val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s |
|
229 |
val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
230 |
|
| 63745 | 231 |
val table_entries = |
232 |
for {
|
|
233 |
((shortcut, conflicts), i) <- shortcut_conflicts zip |
|
234 |
shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length })
|
|
235 |
entry <- |
|
236 |
Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: |
|
237 |
conflicts.map(Table_Entry(_, Some(i), Nil)) |
|
238 |
} yield entry |
|
239 |
||
240 |
val table_model = new Table_Model(table_entries) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
241 |
|
| 63745 | 242 |
if (table_entries.nonEmpty && |
| 63748 | 243 |
GUI.confirm_dialog(view, |
| 63745 | 244 |
"Pending Isabelle/jEdit keymap changes", |
245 |
JOptionPane.OK_CANCEL_OPTION, |
|
| 63753 | 246 |
"The following Isabelle keymap changes are in conflict with the current", |
| 63759 | 247 |
"jEdit keymap " + quote(keymap_name) + ":", |
| 63745 | 248 |
new Table(table_model), |
| 63748 | 249 |
"Selected shortcuts will be applied, unselected changes will be ignored.", |
| 63753 | 250 |
"Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0) |
| 63750 | 251 |
{ table_model.apply(keymap_name, keymap) }
|
252 |
||
253 |
no_shortcut_conflicts.foreach(_.set(keymap)) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
254 |
|
| 63750 | 255 |
keymap.save() |
256 |
jEdit.saveSettings() |
|
|
67648
f6e351043014
more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();
wenzelm
parents:
66923
diff
changeset
|
257 |
jEdit.propertiesChanged() |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
258 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
259 |
} |