# HG changeset patch # User wenzelm # Date 1472650162 -7200 # Node ID 33fb64d7842a7da7cf609867b0be5d422f70db93 # Parent fb0ae6b604910ce32d6fd917a35f8a09940c50bd clarified shortcut conflicts; tuned; diff -r fb0ae6b60491 -r 33fb64d7842a src/Tools/jEdit/src/keymap_merge.scala --- 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())