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