src/Tools/jEdit/src/keymap_merge.scala
author wenzelm
Thu Sep 01 16:05:22 2016 +0200 (2016-09-01)
changeset 63750 9c8a366778e1
parent 63748 ebcc70c120a9
child 63753 c57db6b2befc
permissions -rw-r--r--
more robust persistent storage;
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@63743
    12
import java.lang.{Class, Boolean => JBoolean}
wenzelm@63745
    13
import java.awt.{Color, Dimension, BorderLayout}
wenzelm@63745
    14
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
wenzelm@63737
    15
import javax.swing.table.AbstractTableModel
wenzelm@63734
    16
wenzelm@63734
    17
import scala.collection.JavaConversions
wenzelm@63734
    18
wenzelm@63748
    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@63745
    46
    /* ignore wrt. keymap */
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@63750
    56
    def ignore(keymap_name: String)
wenzelm@63736
    57
    {
wenzelm@63750
    58
      val keymaps1 = Library.insert(keymap_name)(ignored_keymaps()).sorted
wenzelm@63736
    59
      if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
wenzelm@63736
    60
      else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
wenzelm@63736
    61
    }
wenzelm@63745
    62
wenzelm@63745
    63
    def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding)
wenzelm@63745
    64
    def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null)
wenzelm@63734
    65
  }
wenzelm@63734
    66
wenzelm@63745
    67
wenzelm@63745
    68
  /* content wrt. keymap */
wenzelm@63745
    69
wenzelm@63736
    70
  def convert_properties(props: java.util.Properties): List[Shortcut] =
wenzelm@63736
    71
    if (props == null) Nil
wenzelm@63736
    72
    else {
wenzelm@63736
    73
      var result = List.empty[Shortcut]
wenzelm@63736
    74
      for (entry <- JavaConversions.mapAsScalaMap(props)) {
wenzelm@63736
    75
        entry match {
wenzelm@63736
    76
          case (a: String, b: String) if is_shortcut(a) =>
wenzelm@63736
    77
            result ::= new Shortcut(a, b)
wenzelm@63736
    78
          case _ =>
wenzelm@63736
    79
        }
wenzelm@63736
    80
      }
wenzelm@63736
    81
      result.sortBy(_.property)
wenzelm@63736
    82
    }
wenzelm@63736
    83
wenzelm@63745
    84
  def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] =
wenzelm@63734
    85
  {
wenzelm@63736
    86
    val keymap_shortcuts =
wenzelm@63736
    87
      if (keymap == null) Nil
wenzelm@63736
    88
      else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
wenzelm@63736
    89
wenzelm@63745
    90
    for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
wenzelm@63736
    91
      val conflicts =
wenzelm@63736
    92
        keymap_shortcuts.filter(s1 =>
wenzelm@63736
    93
          s.property == s1.property && s.binding != s1.binding ||
wenzelm@63742
    94
          s.property != s1.property && s.binding == s1.binding && s1.binding != "")
wenzelm@63736
    95
      (s, conflicts)
wenzelm@63734
    96
    }
wenzelm@63734
    97
  }
wenzelm@63734
    98
wenzelm@63734
    99
wenzelm@63734
   100
wenzelm@63745
   101
  /** table **/
wenzelm@63737
   102
wenzelm@63739
   103
  private def conflict_color: Color =
wenzelm@63739
   104
    PIDE.options.color_value("error_color")
wenzelm@63739
   105
wenzelm@63740
   106
  private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int])
wenzelm@63737
   107
  {
wenzelm@63738
   108
    override def toString: String =
wenzelm@63740
   109
      if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
wenzelm@63738
   110
      else
wenzelm@63739
   111
        "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
wenzelm@63739
   112
          HTML.output("--- " + shortcut.toString) +
wenzelm@63738
   113
        "</font></html>"
wenzelm@63737
   114
  }
wenzelm@63737
   115
wenzelm@63737
   116
  private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel
wenzelm@63737
   117
  {
wenzelm@63737
   118
    private val entries_count = entries.length
wenzelm@63743
   119
    private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count
wenzelm@63737
   120
    private def get_entry(row: Int): Option[Table_Entry] =
wenzelm@63743
   121
      if (has_entry(row)) Some(entries(row)) else None
wenzelm@63737
   122
wenzelm@63740
   123
    private val selected =
wenzelm@63740
   124
      Synchronized[Set[Int]](
wenzelm@63740
   125
        (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
wenzelm@63737
   126
wenzelm@63745
   127
    private def is_selected(row: Int): Boolean =
wenzelm@63745
   128
      selected.value.contains(row)
wenzelm@63744
   129
wenzelm@63745
   130
    private def select(head: Int, tail: List[Int], b: Boolean): Unit =
wenzelm@63743
   131
      selected.change(set => if (b) set + head -- tail else set - head ++ tail)
wenzelm@63737
   132
wenzelm@63744
   133
    def apply(keymap_name: String, keymap: Keymap)
wenzelm@63744
   134
    {
wenzelm@63744
   135
      GUI_Thread.require {}
wenzelm@63744
   136
wenzelm@63744
   137
      for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
wenzelm@63744
   138
        val b = is_selected(row)
wenzelm@63744
   139
        if (b) {
wenzelm@63745
   140
          entry.tail.foreach(i => entries(i).shortcut.reset(keymap))
wenzelm@63745
   141
          entry.shortcut.set(keymap)
wenzelm@63744
   142
        }
wenzelm@63750
   143
        else
wenzelm@63750
   144
          entry.shortcut.ignore(keymap_name)
wenzelm@63744
   145
      }
wenzelm@63744
   146
    }
wenzelm@63744
   147
wenzelm@63737
   148
    override def getColumnCount: Int = 2
wenzelm@63737
   149
wenzelm@63737
   150
    override def getColumnClass(i: Int): Class[_ <: Object] =
wenzelm@63743
   151
      if (i == 0) classOf[JBoolean] else classOf[Object]
wenzelm@63737
   152
wenzelm@63737
   153
    override def getColumnName(i: Int): String =
wenzelm@63737
   154
      if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???"
wenzelm@63737
   155
wenzelm@63737
   156
    override def getRowCount: Int = entries_count
wenzelm@63737
   157
wenzelm@63737
   158
    override def getValueAt(row: Int, column: Int): AnyRef =
wenzelm@63737
   159
    {
wenzelm@63737
   160
      get_entry(row) match {
wenzelm@63744
   161
        case Some(entry) if column == 0 => JBoolean.valueOf(is_selected(row))
wenzelm@63738
   162
        case Some(entry) if column == 1 => entry
wenzelm@63737
   163
        case _ => null
wenzelm@63737
   164
      }
wenzelm@63737
   165
    }
wenzelm@63739
   166
wenzelm@63739
   167
    override def isCellEditable(row: Int, column: Int): Boolean =
wenzelm@63743
   168
      has_entry(row) && column == 0
wenzelm@63739
   169
wenzelm@63739
   170
    override def setValueAt(value: AnyRef, row: Int, column: Int)
wenzelm@63739
   171
    {
wenzelm@63743
   172
      value match {
wenzelm@63743
   173
        case obj: JBoolean if has_entry(row) && column == 0 =>
wenzelm@63740
   174
          val b = obj.booleanValue
wenzelm@63743
   175
          val entry = entries(row)
wenzelm@63743
   176
          entry.head match {
wenzelm@63743
   177
            case None => select(row, entry.tail, b)
wenzelm@63743
   178
            case Some(head_row) =>
wenzelm@63743
   179
              val head_entry = entries(head_row)
wenzelm@63743
   180
              select(head_row, head_entry.tail, !b)
wenzelm@63740
   181
          }
wenzelm@63743
   182
          GUI_Thread.later { fireTableDataChanged() }
wenzelm@63739
   183
        case _ =>
wenzelm@63739
   184
      }
wenzelm@63739
   185
    }
wenzelm@63737
   186
  }
wenzelm@63737
   187
wenzelm@63745
   188
  private class Table(table_model: Table_Model) extends JPanel(new BorderLayout)
wenzelm@63734
   189
  {
wenzelm@63745
   190
    private val cell_size = GUIUtilities.defaultTableCellSize()
wenzelm@63745
   191
    private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15)
wenzelm@63741
   192
wenzelm@63737
   193
    val table = new JTable(table_model)
wenzelm@63737
   194
    table.setShowGrid(false)
wenzelm@63737
   195
    table.setIntercellSpacing(new Dimension(0, 0))
wenzelm@63741
   196
    table.setRowHeight(cell_size.height + 2)
wenzelm@63741
   197
    table.setPreferredScrollableViewportSize(table_size)
wenzelm@63741
   198
    table.setFillsViewportHeight(true)
wenzelm@63737
   199
    table.getTableHeader.setReorderingAllowed(false)
wenzelm@63734
   200
wenzelm@63745
   201
		table.getColumnModel.getColumn(0).setPreferredWidth(30)
wenzelm@63745
   202
		table.getColumnModel.getColumn(0).setMinWidth(30)
wenzelm@63745
   203
		table.getColumnModel.getColumn(0).setMaxWidth(30)
wenzelm@63745
   204
		table.getColumnModel.getColumn(0).setResizable(false)
wenzelm@63745
   205
		table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
wenzelm@63734
   206
wenzelm@63745
   207
    val scroller = new JScrollPane(table)
wenzelm@63745
   208
		scroller.getViewport.setBackground(table.getBackground)
wenzelm@63745
   209
		scroller.setPreferredSize(table_size)
wenzelm@63734
   210
wenzelm@63745
   211
    add(scroller, BorderLayout.CENTER)
wenzelm@63745
   212
  }
wenzelm@63734
   213
wenzelm@63734
   214
wenzelm@63734
   215
wenzelm@63745
   216
  /** check with optional dialog **/
wenzelm@63745
   217
wenzelm@63748
   218
  def check_dialog(view: View)
wenzelm@63745
   219
  {
wenzelm@63745
   220
    GUI_Thread.require {}
wenzelm@63745
   221
wenzelm@63745
   222
    val keymap_manager = jEdit.getKeymapManager
wenzelm@63745
   223
    val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63745
   224
    val keymap =
wenzelm@63745
   225
      keymap_manager.getKeymap(keymap_name) match {
wenzelm@63745
   226
        case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63745
   227
        case keymap => keymap
wenzelm@63745
   228
      }
wenzelm@63745
   229
wenzelm@63745
   230
    val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap)
wenzelm@63745
   231
    val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s
wenzelm@63745
   232
    val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty)
wenzelm@63734
   233
wenzelm@63745
   234
    val table_entries =
wenzelm@63745
   235
      for {
wenzelm@63745
   236
        ((shortcut, conflicts), i) <- shortcut_conflicts zip
wenzelm@63745
   237
          shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length })
wenzelm@63745
   238
        entry <-
wenzelm@63745
   239
          Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) ::
wenzelm@63745
   240
          conflicts.map(Table_Entry(_, Some(i), Nil))
wenzelm@63745
   241
      } yield entry
wenzelm@63745
   242
wenzelm@63745
   243
    val table_model = new Table_Model(table_entries)
wenzelm@63734
   244
wenzelm@63745
   245
    if (table_entries.nonEmpty &&
wenzelm@63748
   246
        GUI.confirm_dialog(view,
wenzelm@63745
   247
          "Pending Isabelle/jEdit keymap changes",
wenzelm@63745
   248
          JOptionPane.OK_CANCEL_OPTION,
wenzelm@63746
   249
          "The following Isabelle keymap changes are in conflict with",
wenzelm@63745
   250
          "the current jEdit keymap " + quote(keymap_name) + ".",
wenzelm@63745
   251
          new Table(table_model),
wenzelm@63748
   252
          "Selected shortcuts will be applied, unselected changes will be ignored.",
wenzelm@63748
   253
          "Results are made persistent in $JEDIT_SETTINGS/properties.") == 0)
wenzelm@63750
   254
    { table_model.apply(keymap_name, keymap) }
wenzelm@63750
   255
wenzelm@63750
   256
    no_shortcut_conflicts.foreach(_.set(keymap))
wenzelm@63734
   257
wenzelm@63750
   258
    keymap.save()
wenzelm@63750
   259
    keymap_manager.reload()
wenzelm@63750
   260
    jEdit.saveSettings()
wenzelm@63734
   261
  }
wenzelm@63734
   262
}