| author | wenzelm |
| Thu, 01 Sep 2016 16:05:22 +0200 | |
| changeset 63750 | 9c8a366778e1 |
| parent 63748 | ebcc70c120a9 |
| child 63753 | c57db6b2befc |
| 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 |
|
| 63743 | 12 |
import java.lang.{Class, Boolean => JBoolean}
|
| 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] = |
|
51 |
Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
|
|
52 |
||
53 |
def is_ignored(keymap_name: String): Boolean = |
|
54 |
ignored_keymaps().contains(keymap_name) |
|
55 |
||
| 63750 | 56 |
def ignore(keymap_name: String) |
| 63736 | 57 |
{
|
| 63750 | 58 |
val keymaps1 = Library.insert(keymap_name)(ignored_keymaps()).sorted |
| 63736 | 59 |
if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore) |
60 |
else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
|
|
61 |
} |
|
| 63745 | 62 |
|
63 |
def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding) |
|
64 |
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
|
65 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
66 |
|
| 63745 | 67 |
|
68 |
/* content wrt. keymap */ |
|
69 |
||
| 63736 | 70 |
def convert_properties(props: java.util.Properties): List[Shortcut] = |
71 |
if (props == null) Nil |
|
72 |
else {
|
|
73 |
var result = List.empty[Shortcut] |
|
74 |
for (entry <- JavaConversions.mapAsScalaMap(props)) {
|
|
75 |
entry match {
|
|
76 |
case (a: String, b: String) if is_shortcut(a) => |
|
77 |
result ::= new Shortcut(a, b) |
|
78 |
case _ => |
|
79 |
} |
|
80 |
} |
|
81 |
result.sortBy(_.property) |
|
82 |
} |
|
83 |
||
| 63745 | 84 |
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
|
85 |
{
|
| 63736 | 86 |
val keymap_shortcuts = |
87 |
if (keymap == null) Nil |
|
88 |
else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) |
|
89 |
||
| 63745 | 90 |
for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
|
| 63736 | 91 |
val conflicts = |
92 |
keymap_shortcuts.filter(s1 => |
|
93 |
s.property == s1.property && s.binding != s1.binding || |
|
| 63742 | 94 |
s.property != s1.property && s.binding == s1.binding && s1.binding != "") |
| 63736 | 95 |
(s, conflicts) |
|
63734
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 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
98 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
99 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
100 |
|
| 63745 | 101 |
/** table **/ |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
102 |
|
| 63739 | 103 |
private def conflict_color: Color = |
104 |
PIDE.options.color_value("error_color")
|
|
105 |
||
| 63740 | 106 |
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
|
107 |
{
|
| 63738 | 108 |
override def toString: String = |
| 63740 | 109 |
if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" |
| 63738 | 110 |
else |
| 63739 | 111 |
"<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" + |
112 |
HTML.output("--- " + shortcut.toString) +
|
|
| 63738 | 113 |
"</font></html>" |
|
63737
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 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
116 |
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
|
117 |
{
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
118 |
private val entries_count = entries.length |
| 63743 | 119 |
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
|
120 |
private def get_entry(row: Int): Option[Table_Entry] = |
| 63743 | 121 |
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
|
122 |
|
| 63740 | 123 |
private val selected = |
124 |
Synchronized[Set[Int]]( |
|
125 |
(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
|
126 |
|
| 63745 | 127 |
private def is_selected(row: Int): Boolean = |
128 |
selected.value.contains(row) |
|
| 63744 | 129 |
|
| 63745 | 130 |
private def select(head: Int, tail: List[Int], b: Boolean): Unit = |
| 63743 | 131 |
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
|
132 |
|
| 63744 | 133 |
def apply(keymap_name: String, keymap: Keymap) |
134 |
{
|
|
135 |
GUI_Thread.require {}
|
|
136 |
||
137 |
for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
|
|
138 |
val b = is_selected(row) |
|
139 |
if (b) {
|
|
| 63745 | 140 |
entry.tail.foreach(i => entries(i).shortcut.reset(keymap)) |
141 |
entry.shortcut.set(keymap) |
|
| 63744 | 142 |
} |
| 63750 | 143 |
else |
144 |
entry.shortcut.ignore(keymap_name) |
|
| 63744 | 145 |
} |
146 |
} |
|
147 |
||
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
148 |
override def getColumnCount: Int = 2 |
|
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 getColumnClass(i: Int): Class[_ <: Object] = |
| 63743 | 151 |
if (i == 0) classOf[JBoolean] else classOf[Object] |
|
63737
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 getColumnName(i: Int): String = |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
154 |
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
|
155 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
156 |
override def getRowCount: Int = entries_count |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
157 |
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
158 |
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
|
159 |
{
|
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
160 |
get_entry(row) match {
|
| 63744 | 161 |
case Some(entry) if column == 0 => JBoolean.valueOf(is_selected(row)) |
| 63738 | 162 |
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
|
163 |
case _ => null |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
164 |
} |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
165 |
} |
| 63739 | 166 |
|
167 |
override def isCellEditable(row: Int, column: Int): Boolean = |
|
| 63743 | 168 |
has_entry(row) && column == 0 |
| 63739 | 169 |
|
170 |
override def setValueAt(value: AnyRef, row: Int, column: Int) |
|
171 |
{
|
|
| 63743 | 172 |
value match {
|
173 |
case obj: JBoolean if has_entry(row) && column == 0 => |
|
| 63740 | 174 |
val b = obj.booleanValue |
| 63743 | 175 |
val entry = entries(row) |
176 |
entry.head match {
|
|
177 |
case None => select(row, entry.tail, b) |
|
178 |
case Some(head_row) => |
|
179 |
val head_entry = entries(head_row) |
|
180 |
select(head_row, head_entry.tail, !b) |
|
| 63740 | 181 |
} |
| 63743 | 182 |
GUI_Thread.later { fireTableDataChanged() }
|
| 63739 | 183 |
case _ => |
184 |
} |
|
185 |
} |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
186 |
} |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
187 |
|
| 63745 | 188 |
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
|
189 |
{
|
| 63745 | 190 |
private val cell_size = GUIUtilities.defaultTableCellSize() |
191 |
private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) |
|
| 63741 | 192 |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
193 |
val table = new JTable(table_model) |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
194 |
table.setShowGrid(false) |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
195 |
table.setIntercellSpacing(new Dimension(0, 0)) |
| 63741 | 196 |
table.setRowHeight(cell_size.height + 2) |
197 |
table.setPreferredScrollableViewportSize(table_size) |
|
198 |
table.setFillsViewportHeight(true) |
|
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
199 |
table.getTableHeader.setReorderingAllowed(false) |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
200 |
|
| 63745 | 201 |
table.getColumnModel.getColumn(0).setPreferredWidth(30) |
202 |
table.getColumnModel.getColumn(0).setMinWidth(30) |
|
203 |
table.getColumnModel.getColumn(0).setMaxWidth(30) |
|
204 |
table.getColumnModel.getColumn(0).setResizable(false) |
|
205 |
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
|
206 |
|
| 63745 | 207 |
val scroller = new JScrollPane(table) |
208 |
scroller.getViewport.setBackground(table.getBackground) |
|
209 |
scroller.setPreferredSize(table_size) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
210 |
|
| 63745 | 211 |
add(scroller, BorderLayout.CENTER) |
212 |
} |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
213 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
214 |
|
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
215 |
|
| 63745 | 216 |
/** check with optional dialog **/ |
217 |
||
| 63748 | 218 |
def check_dialog(view: View) |
| 63745 | 219 |
{
|
220 |
GUI_Thread.require {}
|
|
221 |
||
222 |
val keymap_manager = jEdit.getKeymapManager |
|
223 |
val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
|
|
224 |
val keymap = |
|
225 |
keymap_manager.getKeymap(keymap_name) match {
|
|
226 |
case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) |
|
227 |
case keymap => keymap |
|
228 |
} |
|
229 |
||
230 |
val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap) |
|
231 |
val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s |
|
232 |
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
|
233 |
|
| 63745 | 234 |
val table_entries = |
235 |
for {
|
|
236 |
((shortcut, conflicts), i) <- shortcut_conflicts zip |
|
237 |
shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length })
|
|
238 |
entry <- |
|
239 |
Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: |
|
240 |
conflicts.map(Table_Entry(_, Some(i), Nil)) |
|
241 |
} yield entry |
|
242 |
||
243 |
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
|
244 |
|
| 63745 | 245 |
if (table_entries.nonEmpty && |
| 63748 | 246 |
GUI.confirm_dialog(view, |
| 63745 | 247 |
"Pending Isabelle/jEdit keymap changes", |
248 |
JOptionPane.OK_CANCEL_OPTION, |
|
| 63746 | 249 |
"The following Isabelle keymap changes are in conflict with", |
| 63745 | 250 |
"the current jEdit keymap " + quote(keymap_name) + ".", |
251 |
new Table(table_model), |
|
| 63748 | 252 |
"Selected shortcuts will be applied, unselected changes will be ignored.", |
253 |
"Results are made persistent in $JEDIT_SETTINGS/properties.") == 0) |
|
| 63750 | 254 |
{ table_model.apply(keymap_name, keymap) }
|
255 |
||
256 |
no_shortcut_conflicts.foreach(_.set(keymap)) |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
257 |
|
| 63750 | 258 |
keymap.save() |
259 |
keymap_manager.reload() |
|
260 |
jEdit.saveSettings() |
|
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
261 |
} |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
262 |
} |