author | wenzelm |
Wed, 31 Aug 2016 21:25:54 +0200 | |
changeset 63740 | 7b2963b11e4a |
parent 63739 | 352a257fa13a |
child 63741 | 10c08a4d39dd |
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 |
63739 | 13 |
import java.awt.{Color, 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 |
|
63739 | 125 |
private def conflict_color: Color = |
126 |
PIDE.options.color_value("error_color") |
|
127 |
||
63740 | 128 |
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
|
129 |
{ |
63738 | 130 |
override def toString: String = |
63740 | 131 |
if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" |
63738 | 132 |
else |
63739 | 133 |
"<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" + |
134 |
HTML.output("--- " + shortcut.toString) + |
|
63738 | 135 |
"</font></html>" |
63737
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 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
138 |
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
|
139 |
{ |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
140 |
private val entries_count = entries.length |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
|
63740 | 144 |
private val selected = |
145 |
Synchronized[Set[Int]]( |
|
146 |
(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
|
147 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
148 |
def select(row: Int, b: Boolean) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
149 |
{ |
63740 | 150 |
if (get_entry(row).isDefined) |
151 |
selected.change(set => if (b) set + row else set - row) |
|
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 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
154 |
def selected_status(row: Int): Option[Boolean] = |
63740 | 155 |
if (get_entry(row).isDefined) Some(selected.value.contains(row)) else None |
63737
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 |
override def getColumnCount: Int = 2 |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
158 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
159 |
override def getColumnClass(i: Int): Class[_ <: Object] = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
160 |
if (i == 0) classOf[java.lang.Boolean] |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
161 |
else classOf[java.lang.Object] |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
162 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
163 |
override def getColumnName(i: Int): String = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
164 |
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
|
165 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
166 |
override def getRowCount: Int = entries_count |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
167 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
168 |
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
|
169 |
{ |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
170 |
get_entry(row) match { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
171 |
case Some(entry) if column == 0 => |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
172 |
selected_status(row) match { |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
173 |
case None => null |
63739 | 174 |
case Some(b) => java.lang.Boolean.valueOf(b) |
63737
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 |
} |
63739 | 180 |
|
181 |
override def isCellEditable(row: Int, column: Int): Boolean = |
|
182 |
get_entry(row) match { |
|
63740 | 183 |
case Some(entry) => column == 0 |
63739 | 184 |
case None => false |
185 |
} |
|
186 |
||
187 |
override def setValueAt(value: AnyRef, row: Int, column: Int) |
|
188 |
{ |
|
189 |
(get_entry(row), value) match { |
|
63740 | 190 |
case (Some(entry), obj: java.lang.Boolean) if entry.head.isEmpty && column == 0 => |
191 |
val b = obj.booleanValue |
|
192 |
select(row, b) |
|
193 |
if (entry.tail.nonEmpty) { |
|
194 |
entry.tail.foreach(select(_, !b)) |
|
195 |
GUI_Thread.later { fireTableDataChanged() } |
|
196 |
} |
|
63739 | 197 |
case _ => |
198 |
} |
|
199 |
} |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
200 |
} |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
201 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
202 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
203 |
|
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
204 |
/** dialog **/ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
205 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
206 |
def check_dialog(view: View) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
207 |
{ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
208 |
GUI_Thread.require {} |
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
209 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
210 |
val (keymap_name, keymap) = get_keymap() |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
211 |
val shortcut_conflicts = get_shortcut_conflicts(keymap) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
212 |
|
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
213 |
val pending_conflicts = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
// FIXME else silent change |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
217 |
} |
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 |
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
|
220 |
extends JDialog(view) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
221 |
{ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
222 |
/* table */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
223 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
224 |
val table_entries = |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
225 |
for { |
63740 | 226 |
((shortcut, conflicts), i) <- shortcut_conflicts zip |
227 |
shortcut_conflicts.scanLeft(0)({ case (i, (_, conflicts)) => i + 1 + conflicts.length }) |
|
228 |
entry <- |
|
229 |
Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: |
|
230 |
conflicts.map(Table_Entry(_, Some(i), Nil)) |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
231 |
} yield entry |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
232 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
233 |
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
|
234 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
235 |
val table = new JTable(table_model) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
236 |
table.setShowGrid(false) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
237 |
table.setIntercellSpacing(new Dimension(0, 0)) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
238 |
table.setRowHeight(GUIUtilities.defaultRowHeight() + 2) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
239 |
table.setPreferredScrollableViewportSize(new Dimension(500, 300)) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
240 |
table.getTableHeader.setReorderingAllowed(false) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
241 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
242 |
val col0 = table.getColumnModel.getColumn(0) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
243 |
val col1 = table.getColumnModel.getColumn(1) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
244 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
245 |
col0.setPreferredWidth(30) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
246 |
col0.setMinWidth(30) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
247 |
col0.setMaxWidth(30) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
248 |
col0.setResizable(false) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
249 |
|
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
250 |
col1.setPreferredWidth(300) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
251 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
252 |
val table_scroller = new JScrollPane(table) |
63737
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
253 |
table_scroller.getViewport.setBackground(table.getBackground) |
6de6e883c5fb
more table content, similar to org.gjt.sp.jedit.pluginmgr.ManagePanel;
wenzelm
parents:
63736
diff
changeset
|
254 |
table_scroller.setPreferredSize(new Dimension(400, 400)) |
63734
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
255 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
256 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
257 |
/* buttons */ |
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 |
val ok_button = new Button("OK") { |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
260 |
reactions += { case ButtonClicked(_) => close() } // FIXME |
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 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
263 |
val cancel_button = new Button("Cancel") { |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
264 |
reactions += { case ButtonClicked(_) => close() } // FIXME |
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 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
267 |
private def close() |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
268 |
{ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
269 |
setVisible(false) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
270 |
dispose() |
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 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
273 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
274 |
/* layout */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
275 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
276 |
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
|
277 |
private val layout_panel = new BorderPanel |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
278 |
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
|
279 |
layout_panel.layout(action_panel) = BorderPanel.Position.South |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
280 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
281 |
setContentPane(layout_panel.peer) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
282 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
283 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
284 |
/* main */ |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
285 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
286 |
setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
287 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
288 |
setTitle("Isabelle/jEdit keymap changes") |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
289 |
|
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
290 |
pack() |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
291 |
setLocationRelativeTo(view) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
292 |
setVisible(true) |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
293 |
} |
133e3e84e6fb
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents:
diff
changeset
|
294 |
} |