src/Tools/jEdit/src/keymap_merge.scala
author wenzelm
Wed Aug 31 15:29:22 2016 +0200 (2016-08-31)
changeset 63736 33fb64d7842a
parent 63734 133e3e84e6fb
child 63737 6de6e883c5fb
permissions -rw-r--r--
clarified shortcut conflicts;
tuned;
wenzelm@63734
     1
/*  Title:      Tools/jEdit/src/keymap_merge.scala
wenzelm@63734
     2
    Author:     Makarius
wenzelm@63734
     3
wenzelm@63736
     4
Merge of Isabelle shortcuts vs. jEdit keymap.
wenzelm@63734
     5
*/
wenzelm@63734
     6
wenzelm@63734
     7
package isabelle.jedit
wenzelm@63734
     8
wenzelm@63734
     9
wenzelm@63734
    10
import isabelle._
wenzelm@63734
    11
wenzelm@63734
    12
import java.awt.event.WindowEvent
wenzelm@63734
    13
import javax.swing.{WindowConstants, JDialog, JTable, JScrollPane}
wenzelm@63734
    14
wenzelm@63734
    15
import scala.collection.JavaConversions
wenzelm@63734
    16
import scala.swing.{FlowPanel, BorderPanel, Component, Button}
wenzelm@63734
    17
import scala.swing.event.ButtonClicked
wenzelm@63734
    18
wenzelm@63734
    19
import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
wenzelm@63734
    20
import org.jedit.keymap.{KeymapManager, Keymap}
wenzelm@63734
    21
wenzelm@63734
    22
wenzelm@63734
    23
object Keymap_Merge
wenzelm@63734
    24
{
wenzelm@63736
    25
  /** shortcuts **/
wenzelm@63734
    26
wenzelm@63736
    27
  private def is_shortcut(property: String): Boolean =
wenzelm@63736
    28
    (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
wenzelm@63736
    29
    !property.startsWith("options.shortcuts.")
wenzelm@63736
    30
wenzelm@63736
    31
  class Shortcut(val property: String, val binding: String)
wenzelm@63734
    32
  {
wenzelm@63736
    33
    override def toString: String = property + "=" + binding
wenzelm@63736
    34
wenzelm@63736
    35
    def primary: Boolean = property.endsWith(".shortcut")
wenzelm@63734
    36
wenzelm@63736
    37
    val action: String =
wenzelm@63736
    38
      Library.try_unsuffix(".shortcut", property) orElse
wenzelm@63736
    39
      Library.try_unsuffix(".shortcut2", property) getOrElse
wenzelm@63736
    40
      error("Bad shortcut property: " + quote(property))
wenzelm@63736
    41
wenzelm@63734
    42
    val label: String =
wenzelm@63734
    43
      GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
wenzelm@63736
    44
wenzelm@63736
    45
wenzelm@63736
    46
    /* ignore wrt. keymaps */
wenzelm@63736
    47
wenzelm@63736
    48
    private def prop_ignore: String = property + ".ignore"
wenzelm@63736
    49
wenzelm@63736
    50
    def ignored_keymaps(): List[String] =
wenzelm@63736
    51
      Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
wenzelm@63736
    52
wenzelm@63736
    53
    def is_ignored(keymap_name: String): Boolean =
wenzelm@63736
    54
      ignored_keymaps().contains(keymap_name)
wenzelm@63736
    55
wenzelm@63736
    56
    def update_ignored(keymap_name: String, ignore: Boolean)
wenzelm@63736
    57
    {
wenzelm@63736
    58
      val keymaps1 =
wenzelm@63736
    59
        if (ignore) Library.insert(keymap_name)(ignored_keymaps()).sorted
wenzelm@63736
    60
        else Library.remove(keymap_name)(ignored_keymaps())
wenzelm@63736
    61
wenzelm@63736
    62
      if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
wenzelm@63736
    63
      else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
wenzelm@63736
    64
    }
wenzelm@63734
    65
  }
wenzelm@63734
    66
wenzelm@63736
    67
  def convert_properties(props: java.util.Properties): List[Shortcut] =
wenzelm@63736
    68
    if (props == null) Nil
wenzelm@63736
    69
    else {
wenzelm@63736
    70
      var result = List.empty[Shortcut]
wenzelm@63736
    71
      for (entry <- JavaConversions.mapAsScalaMap(props)) {
wenzelm@63736
    72
        entry match {
wenzelm@63736
    73
          case (a: String, b: String) if is_shortcut(a) =>
wenzelm@63736
    74
            result ::= new Shortcut(a, b)
wenzelm@63736
    75
          case _ =>
wenzelm@63736
    76
        }
wenzelm@63736
    77
      }
wenzelm@63736
    78
      result.sortBy(_.property)
wenzelm@63736
    79
    }
wenzelm@63736
    80
wenzelm@63736
    81
wenzelm@63736
    82
  /* keymap */
wenzelm@63736
    83
wenzelm@63736
    84
  def get_keymap(): (String, Keymap) =
wenzelm@63734
    85
  {
wenzelm@63736
    86
    val manager = jEdit.getKeymapManager
wenzelm@63736
    87
    val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63736
    88
    val keymap =
wenzelm@63736
    89
      manager.getKeymap(keymap_name) match {
wenzelm@63736
    90
        case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63736
    91
        case keymap => keymap
wenzelm@63734
    92
      }
wenzelm@63736
    93
    (keymap_name, keymap)
wenzelm@63734
    94
  }
wenzelm@63734
    95
wenzelm@63736
    96
  def change_keymap(keymap: Keymap, entry: (Shortcut, List[Shortcut]))
wenzelm@63736
    97
  {
wenzelm@63736
    98
    val (shortcut, conflicts) = entry
wenzelm@63736
    99
    conflicts.foreach(s => keymap.setShortcut(s.property, ""))
wenzelm@63736
   100
    keymap.setShortcut(shortcut.property, shortcut.binding)
wenzelm@63736
   101
  }
wenzelm@63734
   102
wenzelm@63736
   103
  def shortcut_conflicts(show_all: Boolean = false): List[(Shortcut, List[Shortcut])] =
wenzelm@63734
   104
  {
wenzelm@63736
   105
    val (keymap_name, keymap) = get_keymap()
wenzelm@63736
   106
    val keymap_shortcuts =
wenzelm@63736
   107
      if (keymap == null) Nil
wenzelm@63736
   108
      else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
wenzelm@63736
   109
wenzelm@63736
   110
    for {
wenzelm@63736
   111
      s <- convert_properties(jEdit.getProperties)
wenzelm@63736
   112
      if show_all || !s.is_ignored(keymap_name)
wenzelm@63736
   113
    }
wenzelm@63736
   114
    yield {
wenzelm@63736
   115
      val conflicts =
wenzelm@63736
   116
        keymap_shortcuts.filter(s1 =>
wenzelm@63736
   117
          s.property == s1.property && s.binding != s1.binding ||
wenzelm@63736
   118
          s.property != s1.property && s.binding == s1.binding)
wenzelm@63736
   119
      (s, conflicts)
wenzelm@63734
   120
    }
wenzelm@63734
   121
  }
wenzelm@63734
   122
wenzelm@63734
   123
wenzelm@63734
   124
wenzelm@63734
   125
  /** dialog **/
wenzelm@63734
   126
wenzelm@63734
   127
  def dialog(view: View)
wenzelm@63734
   128
  {
wenzelm@63734
   129
    GUI_Thread.require {}
wenzelm@63734
   130
    new Dialog(view)
wenzelm@63734
   131
  }
wenzelm@63734
   132
wenzelm@63734
   133
  private class Dialog(view: View) extends JDialog(view)
wenzelm@63734
   134
  {
wenzelm@63734
   135
    /* table */
wenzelm@63734
   136
wenzelm@63736
   137
    val shortcuts = List.empty[Shortcut]
wenzelm@63734
   138
wenzelm@63734
   139
    def get_label(action: String): String =
wenzelm@63734
   140
      shortcuts.collectFirst(
wenzelm@63734
   141
        { case s if s.action == action && s.label != "" => s.label }).getOrElse(action)
wenzelm@63734
   142
wenzelm@63736
   143
    def get_binding(action: String, primary: Boolean): String =
wenzelm@63734
   144
      shortcuts.collectFirst(
wenzelm@63736
   145
        { case s if s.action == action && s.primary == primary => s.binding }).getOrElse("")
wenzelm@63734
   146
wenzelm@63734
   147
    val column_names: Array[AnyRef] =
wenzelm@63734
   148
      Array(jEdit.getProperty("options.shortcuts.name"),
wenzelm@63734
   149
        jEdit.getProperty("options.shortcuts.shortcut1"),
wenzelm@63734
   150
        jEdit.getProperty("options.shortcuts.shortcut2"))
wenzelm@63734
   151
wenzelm@63734
   152
    val table_rows: Array[Array[AnyRef]] =
wenzelm@63736
   153
      shortcuts.map(s =>
wenzelm@63736
   154
        Array[AnyRef](s.label, get_binding(s.action, true), get_binding(s.action, false))).toArray
wenzelm@63734
   155
wenzelm@63734
   156
    val table = new JTable(table_rows, column_names)
wenzelm@63734
   157
    table.setRowHeight(GUIUtilities.defaultRowHeight())
wenzelm@63734
   158
    table.getTableHeader().setReorderingAllowed(false)  // FIXME !?
wenzelm@63734
   159
wenzelm@63734
   160
    val table_size = table.getPreferredSize()
wenzelm@63734
   161
    table_size.height = table_size.height min 200
wenzelm@63734
   162
wenzelm@63734
   163
    val table_scroller = new JScrollPane(table)
wenzelm@63734
   164
    table_scroller.setPreferredSize(table_size)
wenzelm@63734
   165
wenzelm@63734
   166
wenzelm@63734
   167
    /* buttons */
wenzelm@63734
   168
wenzelm@63734
   169
    val ok_button = new Button("OK") {
wenzelm@63734
   170
      reactions += { case ButtonClicked(_) => close() }  // FIXME
wenzelm@63734
   171
    }
wenzelm@63734
   172
wenzelm@63734
   173
    val cancel_button = new Button("Cancel") {
wenzelm@63734
   174
      reactions += { case ButtonClicked(_) => close() }  // FIXME
wenzelm@63734
   175
    }
wenzelm@63734
   176
wenzelm@63734
   177
    private def close()
wenzelm@63734
   178
    {
wenzelm@63734
   179
      setVisible(false)
wenzelm@63734
   180
      dispose()
wenzelm@63734
   181
    }
wenzelm@63734
   182
wenzelm@63734
   183
wenzelm@63734
   184
    /* layout */
wenzelm@63734
   185
wenzelm@63734
   186
    private val action_panel = new FlowPanel(FlowPanel.Alignment.Right)(ok_button, cancel_button)
wenzelm@63734
   187
    private val layout_panel = new BorderPanel
wenzelm@63734
   188
    layout_panel.layout(Component.wrap(table_scroller)) = BorderPanel.Position.Center
wenzelm@63734
   189
    layout_panel.layout(action_panel) = BorderPanel.Position.South
wenzelm@63734
   190
wenzelm@63734
   191
    setContentPane(layout_panel.peer)
wenzelm@63734
   192
wenzelm@63734
   193
wenzelm@63734
   194
    /* main */
wenzelm@63734
   195
wenzelm@63734
   196
    setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE)
wenzelm@63734
   197
wenzelm@63734
   198
    setTitle("Isabelle/jEdit keymap changes")
wenzelm@63734
   199
wenzelm@63734
   200
    pack()
wenzelm@63734
   201
    setLocationRelativeTo(view)
wenzelm@63734
   202
    setVisible(true)
wenzelm@63734
   203
  }
wenzelm@63734
   204
}