author | wenzelm |
Wed, 31 Aug 2016 18:33:42 +0200 | |
changeset 63738 | f215f5f5bd35 |
parent 63737 | 6de6e883c5fb |
child 63739 | 352a257fa13a |
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 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
12 |
import java.lang.Class |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
13 |
import java.awt.Dimension |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
14 |
import java.awt.event.WindowEvent |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
15 |
import javax.swing.{WindowConstants, JDialog, JTable, JScrollPane} |
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
16 |
import javax.swing.table.AbstractTableModel |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
17 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
18 |
import scala.collection.JavaConversions |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
19 |
import scala.swing.{FlowPanel, BorderPanel, Component, Button} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
20 |
import scala.swing.event.ButtonClicked |
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 |
import org.gjt.sp.jedit.{jEdit, View, GUIUtilities} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
23 |
import org.jedit.keymap.{KeymapManager, Keymap} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
24 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
25 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
26 |
object Keymap_Merge |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
27 |
{ |
63736 | 28 |
/** shortcuts **/ |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
29 |
|
63736 | 30 |
private def is_shortcut(property: String): Boolean = |
31 |
(property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && |
|
32 |
!property.startsWith("options.shortcuts.") |
|
33 |
||
34 |
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
|
35 |
{ |
63736 | 36 |
override def toString: String = property + "=" + binding |
37 |
||
38 |
def primary: Boolean = property.endsWith(".shortcut") |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
39 |
|
63736 | 40 |
val action: String = |
41 |
Library.try_unsuffix(".shortcut", property) orElse |
|
42 |
Library.try_unsuffix(".shortcut2", property) getOrElse |
|
43 |
error("Bad shortcut property: " + quote(property)) |
|
44 |
||
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
45 |
val label: String = |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
46 |
GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) |
63736 | 47 |
|
48 |
||
49 |
/* ignore wrt. keymaps */ |
|
50 |
||
51 |
private def prop_ignore: String = property + ".ignore" |
|
52 |
||
53 |
def ignored_keymaps(): List[String] = |
|
54 |
Library.space_explode(',', jEdit.getProperty(prop_ignore, "")) |
|
55 |
||
56 |
def is_ignored(keymap_name: String): Boolean = |
|
57 |
ignored_keymaps().contains(keymap_name) |
|
58 |
||
59 |
def update_ignored(keymap_name: String, ignore: Boolean) |
|
60 |
{ |
|
61 |
val keymaps1 = |
|
62 |
if (ignore) Library.insert(keymap_name)(ignored_keymaps()).sorted |
|
63 |
else Library.remove(keymap_name)(ignored_keymaps()) |
|
64 |
||
65 |
if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore) |
|
66 |
else jEdit.setProperty(prop_ignore, keymaps1.mkString(",")) |
|
67 |
} |
|
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 |
|
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 |
||
84 |
||
85 |
/* keymap */ |
|
86 |
||
87 |
def get_keymap(): (String, Keymap) = |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
88 |
{ |
63736 | 89 |
val manager = jEdit.getKeymapManager |
90 |
val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) |
|
91 |
val keymap = |
|
92 |
manager.getKeymap(keymap_name) match { |
|
93 |
case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) |
|
94 |
case keymap => keymap |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
95 |
} |
63736 | 96 |
(keymap_name, keymap) |
63734
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 |
|
63736 | 99 |
def change_keymap(keymap: Keymap, entry: (Shortcut, List[Shortcut])) |
100 |
{ |
|
101 |
val (shortcut, conflicts) = entry |
|
102 |
conflicts.foreach(s => keymap.setShortcut(s.property, "")) |
|
103 |
keymap.setShortcut(shortcut.property, shortcut.binding) |
|
104 |
} |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
105 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
106 |
def get_shortcut_conflicts(keymap: Keymap): List[(Shortcut, List[Shortcut])] = |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
107 |
{ |
63736 | 108 |
val keymap_shortcuts = |
109 |
if (keymap == null) Nil |
|
110 |
else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) |
|
111 |
||
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
112 |
for (s <- convert_properties(jEdit.getProperties)) yield { |
63736 | 113 |
val conflicts = |
114 |
keymap_shortcuts.filter(s1 => |
|
115 |
s.property == s1.property && s.binding != s1.binding || |
|
116 |
s.property != s1.property && s.binding == s1.binding) |
|
117 |
(s, conflicts) |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
118 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
119 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
120 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
121 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
122 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
123 |
/** table model **/ |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
124 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
125 |
private sealed case class Table_Entry(shortcut: Shortcut, head: Boolean) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
126 |
{ |
63738 | 127 |
override def toString: String = |
128 |
if (head) "<html>" + HTML.output(shortcut.toString) + "</html>" |
|
129 |
else |
|
130 |
"<html><font style='color: #B22222;'>" + |
|
131 |
HTML.output(" -- " + shortcut.toString) + |
|
132 |
"</font></html>" |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
133 |
} |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
134 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
135 |
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
|
136 |
{ |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
137 |
private val entries_count = entries.length |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
138 |
private def get_entry(row: Int): Option[Table_Entry] = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
139 |
if (0 <= row && row <= entries_count) Some(entries(row)) else None |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
140 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
141 |
private val ignored = Synchronized(Set.empty[Shortcut]) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
142 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
143 |
def select(row: Int, b: Boolean) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
144 |
{ |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
145 |
for (entry <- get_entry(row) if entry.head) { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
146 |
ignored.change(set => if (b) set - entry.shortcut else set + entry.shortcut) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
147 |
} |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
148 |
} |
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 |
def selected_status(row: Int): Option[Boolean] = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
151 |
get_entry(row) match { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
152 |
case Some(entry) if entry.head => Some(!ignored.value.contains(entry.shortcut)) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
153 |
case _ => None |
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 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
156 |
override def getColumnCount: Int = 2 |
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 getColumnClass(i: Int): Class[_ <: Object] = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
159 |
if (i == 0) classOf[java.lang.Boolean] |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
160 |
else classOf[java.lang.Object] |
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 |
override def getColumnName(i: Int): String = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
163 |
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
|
164 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
165 |
override def getRowCount: Int = entries_count |
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 |
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
|
168 |
{ |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
169 |
get_entry(row) match { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
170 |
case Some(entry) if column == 0 => |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
171 |
selected_status(row) match { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
172 |
case None => null |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
173 |
case Some(true) => java.lang.Boolean.TRUE |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
174 |
case Some(false) => java.lang.Boolean.FALSE |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
175 |
} |
63738 | 176 |
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
|
177 |
case _ => null |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
178 |
} |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
179 |
} |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
180 |
} |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
181 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
182 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
183 |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
184 |
/** dialog **/ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
185 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
186 |
def check_dialog(view: View) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
187 |
{ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
188 |
GUI_Thread.require {} |
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
189 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
190 |
val (keymap_name, keymap) = get_keymap() |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
191 |
val shortcut_conflicts = get_shortcut_conflicts(keymap) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
192 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
193 |
val pending_conflicts = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
194 |
shortcut_conflicts.filter({ case (s, cs) => !s.is_ignored(keymap_name) && cs.nonEmpty }) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
195 |
if (pending_conflicts.nonEmpty) new Dialog(view, pending_conflicts) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
196 |
// FIXME else silent change |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
197 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
198 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
199 |
private class Dialog(view: View, shortcut_conflicts: List[(Shortcut, List[Shortcut])]) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
200 |
extends JDialog(view) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
201 |
{ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
202 |
/* table */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
203 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
204 |
val table_entries = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
205 |
for { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
206 |
(shortcut, conflicts) <- shortcut_conflicts |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
207 |
entry <- Table_Entry(shortcut, true) :: conflicts.map(Table_Entry(_, false)) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
208 |
} yield entry |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
209 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
210 |
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
|
211 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
212 |
val table = new JTable(table_model) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
213 |
table.setShowGrid(false) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
214 |
table.setIntercellSpacing(new Dimension(0, 0)) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
215 |
table.setRowHeight(GUIUtilities.defaultRowHeight() + 2) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
216 |
table.setPreferredScrollableViewportSize(new Dimension(500, 300)) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
217 |
table.getTableHeader.setReorderingAllowed(false) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
218 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
219 |
val col0 = table.getColumnModel.getColumn(0) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
220 |
val col1 = table.getColumnModel.getColumn(1) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
221 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
222 |
col0.setPreferredWidth(30) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
223 |
col0.setMinWidth(30) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
224 |
col0.setMaxWidth(30) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
225 |
col0.setResizable(false) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
226 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
227 |
col1.setPreferredWidth(300) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
228 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
229 |
val table_scroller = new JScrollPane(table) |
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
230 |
table_scroller.getViewport.setBackground(table.getBackground) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
231 |
table_scroller.setPreferredSize(new Dimension(400, 400)) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
232 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
233 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
234 |
/* buttons */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
235 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
236 |
val ok_button = new Button("OK") { |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
237 |
reactions += { case ButtonClicked(_) => close() } // FIXME |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
238 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
239 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
240 |
val cancel_button = new Button("Cancel") { |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
241 |
reactions += { case ButtonClicked(_) => close() } // FIXME |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
242 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
243 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
244 |
private def close() |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
245 |
{ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
246 |
setVisible(false) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
247 |
dispose() |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
248 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
249 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
250 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
251 |
/* layout */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
252 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
253 |
private val action_panel = new FlowPanel(FlowPanel.Alignment.Right)(ok_button, cancel_button) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
254 |
private val layout_panel = new BorderPanel |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
255 |
layout_panel.layout(Component.wrap(table_scroller)) = BorderPanel.Position.Center |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
256 |
layout_panel.layout(action_panel) = BorderPanel.Position.South |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
257 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
258 |
setContentPane(layout_panel.peer) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
259 |
|
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 |
/* main */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
262 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
263 |
setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
264 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
265 |
setTitle("Isabelle/jEdit keymap changes") |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
266 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
267 |
pack() |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
268 |
setLocationRelativeTo(view) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
269 |
setVisible(true) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
270 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
271 |
} |