--- a/src/Tools/jEdit/src/keymap_merge.scala Wed Aug 31 10:49:30 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala Wed Aug 31 15:29:22 2016 +0200
@@ -1,7 +1,7 @@
/* Title: Tools/jEdit/src/keymap_merge.scala
Author: Makarius
-Merge of Isabelle/jEdit shortcuts wrt. jEdit keymap.
+Merge of Isabelle shortcuts vs. jEdit keymap.
*/
package isabelle.jedit
@@ -12,9 +12,7 @@
import java.awt.event.WindowEvent
import javax.swing.{WindowConstants, JDialog, JTable, JScrollPane}
-import scala.collection.mutable
import scala.collection.JavaConversions
-import scala.collection.immutable.SortedSet
import scala.swing.{FlowPanel, BorderPanel, Component, Button}
import scala.swing.event.ButtonClicked
@@ -24,44 +22,101 @@
object Keymap_Merge
{
- /* Isabelle/jEdit shortcuts */
+ /** shortcuts **/
- sealed case class Shortcut(action: String, key: String, alternative: Boolean)
+ private def is_shortcut(property: String): Boolean =
+ (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
+ !property.startsWith("options.shortcuts.")
+
+ class Shortcut(val property: String, val binding: String)
{
- def eq_action(that: Shortcut): Boolean = action == that.action
+ override def toString: String = property + "=" + binding
+
+ def primary: Boolean = property.endsWith(".shortcut")
- val property: String = if (alternative) action + ".shortcut2" else action + ".shortcut"
+ val action: String =
+ Library.try_unsuffix(".shortcut", property) orElse
+ Library.try_unsuffix(".shortcut2", property) getOrElse
+ error("Bad shortcut property: " + quote(property))
+
val label: String =
GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
+
+
+ /* ignore wrt. keymaps */
+
+ private def prop_ignore: String = property + ".ignore"
+
+ def ignored_keymaps(): List[String] =
+ Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
+
+ def is_ignored(keymap_name: String): Boolean =
+ ignored_keymaps().contains(keymap_name)
+
+ def update_ignored(keymap_name: String, ignore: Boolean)
+ {
+ val keymaps1 =
+ if (ignore) Library.insert(keymap_name)(ignored_keymaps()).sorted
+ else Library.remove(keymap_name)(ignored_keymaps())
+
+ if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
+ else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
+ }
}
- def additional_shortcuts(): List[Shortcut] =
+ def convert_properties(props: java.util.Properties): List[Shortcut] =
+ if (props == null) Nil
+ else {
+ var result = List.empty[Shortcut]
+ for (entry <- JavaConversions.mapAsScalaMap(props)) {
+ entry match {
+ case (a: String, b: String) if is_shortcut(a) =>
+ result ::= new Shortcut(a, b)
+ case _ =>
+ }
+ }
+ result.sortBy(_.property)
+ }
+
+
+ /* keymap */
+
+ def get_keymap(): (String, Keymap) =
{
- val result = new mutable.ListBuffer[Shortcut]
- for (entry <- JavaConversions.mapAsScalaMap(jEdit.getProperties)) {
- entry match {
- case (a: String, b: String) if a.endsWith(".shortcut") =>
- val action = a.substring(0, a.length - 9)
- result += Shortcut(action, b, false)
- case (a: String, b: String) if a.endsWith(".shortcut2") =>
- val action = a.substring(0, a.length - 10)
- result += Shortcut(action, b, true)
- case _ =>
+ val manager = jEdit.getKeymapManager
+ val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
+ val keymap =
+ manager.getKeymap(keymap_name) match {
+ case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
+ case keymap => keymap
}
- }
- result.toList
+ (keymap_name, keymap)
}
+ def change_keymap(keymap: Keymap, entry: (Shortcut, List[Shortcut]))
+ {
+ val (shortcut, conflicts) = entry
+ conflicts.foreach(s => keymap.setShortcut(s.property, ""))
+ keymap.setShortcut(shortcut.property, shortcut.binding)
+ }
- /* jEdit keymap */
-
- def current_keymap(): Keymap =
+ def shortcut_conflicts(show_all: Boolean = false): List[(Shortcut, List[Shortcut])] =
{
- val manager = jEdit.getKeymapManager
- val name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
- manager.getKeymap(name) match {
- case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
- case keymap => keymap
+ val (keymap_name, keymap) = get_keymap()
+ val keymap_shortcuts =
+ if (keymap == null) Nil
+ else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
+
+ for {
+ s <- convert_properties(jEdit.getProperties)
+ if show_all || !s.is_ignored(keymap_name)
+ }
+ yield {
+ val conflicts =
+ keymap_shortcuts.filter(s1 =>
+ s.property == s1.property && s.binding != s1.binding ||
+ s.property != s1.property && s.binding == s1.binding)
+ (s, conflicts)
}
}
@@ -79,15 +134,15 @@
{
/* table */
- val shortcuts = additional_shortcuts()
+ val shortcuts = List.empty[Shortcut]
def get_label(action: String): String =
shortcuts.collectFirst(
{ case s if s.action == action && s.label != "" => s.label }).getOrElse(action)
- def get_key(action: String, alternative: Boolean): String =
+ def get_binding(action: String, primary: Boolean): String =
shortcuts.collectFirst(
- { case s if s.action == action && s.alternative == alternative => s.key }).getOrElse("")
+ { case s if s.action == action && s.primary == primary => s.binding }).getOrElse("")
val column_names: Array[AnyRef] =
Array(jEdit.getProperty("options.shortcuts.name"),
@@ -95,8 +150,8 @@
jEdit.getProperty("options.shortcuts.shortcut2"))
val table_rows: Array[Array[AnyRef]] =
- Library.distinct[Shortcut](shortcuts, _ eq_action _).sortBy(_.action).
- map(s => Array[AnyRef](s.label, get_key(s.action, false), get_key(s.action, true))).toArray
+ shortcuts.map(s =>
+ Array[AnyRef](s.label, get_binding(s.action, true), get_binding(s.action, false))).toArray
val table = new JTable(table_rows, column_names)
table.setRowHeight(GUIUtilities.defaultRowHeight())