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