src/Tools/jEdit/src/keymap_merge.scala
author wenzelm
Wed Aug 31 21:25:54 2016 +0200 (2016-08-31)
changeset 63740 7b2963b11e4a
parent 63739 352a257fa13a
child 63741 10c08a4d39dd
permissions -rw-r--r--
clarified GUI;
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@63737
    12
import java.lang.Class
wenzelm@63739
    13
import java.awt.{Color, Dimension}
wenzelm@63734
    14
import java.awt.event.WindowEvent
wenzelm@63734
    15
import javax.swing.{WindowConstants, JDialog, JTable, JScrollPane}
wenzelm@63737
    16
import javax.swing.table.AbstractTableModel
wenzelm@63734
    17
wenzelm@63734
    18
import scala.collection.JavaConversions
wenzelm@63734
    19
import scala.swing.{FlowPanel, BorderPanel, Component, Button}
wenzelm@63734
    20
import scala.swing.event.ButtonClicked
wenzelm@63734
    21
wenzelm@63734
    22
import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
wenzelm@63734
    23
import org.jedit.keymap.{KeymapManager, Keymap}
wenzelm@63734
    24
wenzelm@63734
    25
wenzelm@63734
    26
object Keymap_Merge
wenzelm@63734
    27
{
wenzelm@63736
    28
  /** shortcuts **/
wenzelm@63734
    29
wenzelm@63736
    30
  private def is_shortcut(property: String): Boolean =
wenzelm@63736
    31
    (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
wenzelm@63736
    32
    !property.startsWith("options.shortcuts.")
wenzelm@63736
    33
wenzelm@63736
    34
  class Shortcut(val property: String, val binding: String)
wenzelm@63734
    35
  {
wenzelm@63736
    36
    override def toString: String = property + "=" + binding
wenzelm@63736
    37
wenzelm@63736
    38
    def primary: Boolean = property.endsWith(".shortcut")
wenzelm@63734
    39
wenzelm@63736
    40
    val action: String =
wenzelm@63736
    41
      Library.try_unsuffix(".shortcut", property) orElse
wenzelm@63736
    42
      Library.try_unsuffix(".shortcut2", property) getOrElse
wenzelm@63736
    43
      error("Bad shortcut property: " + quote(property))
wenzelm@63736
    44
wenzelm@63734
    45
    val label: String =
wenzelm@63734
    46
      GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
wenzelm@63736
    47
wenzelm@63736
    48
wenzelm@63736
    49
    /* ignore wrt. keymaps */
wenzelm@63736
    50
wenzelm@63736
    51
    private def prop_ignore: String = property + ".ignore"
wenzelm@63736
    52
wenzelm@63736
    53
    def ignored_keymaps(): List[String] =
wenzelm@63736
    54
      Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
wenzelm@63736
    55
wenzelm@63736
    56
    def is_ignored(keymap_name: String): Boolean =
wenzelm@63736
    57
      ignored_keymaps().contains(keymap_name)
wenzelm@63736
    58
wenzelm@63736
    59
    def update_ignored(keymap_name: String, ignore: Boolean)
wenzelm@63736
    60
    {
wenzelm@63736
    61
      val keymaps1 =
wenzelm@63736
    62
        if (ignore) Library.insert(keymap_name)(ignored_keymaps()).sorted
wenzelm@63736
    63
        else Library.remove(keymap_name)(ignored_keymaps())
wenzelm@63736
    64
wenzelm@63736
    65
      if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
wenzelm@63736
    66
      else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
wenzelm@63736
    67
    }
wenzelm@63734
    68
  }
wenzelm@63734
    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@63736
    84
wenzelm@63736
    85
  /* keymap */
wenzelm@63736
    86
wenzelm@63736
    87
  def get_keymap(): (String, Keymap) =
wenzelm@63734
    88
  {
wenzelm@63736
    89
    val manager = jEdit.getKeymapManager
wenzelm@63736
    90
    val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63736
    91
    val keymap =
wenzelm@63736
    92
      manager.getKeymap(keymap_name) match {
wenzelm@63736
    93
        case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63736
    94
        case keymap => keymap
wenzelm@63734
    95
      }
wenzelm@63736
    96
    (keymap_name, keymap)
wenzelm@63734
    97
  }
wenzelm@63734
    98
wenzelm@63736
    99
  def change_keymap(keymap: Keymap, entry: (Shortcut, List[Shortcut]))
wenzelm@63736
   100
  {
wenzelm@63736
   101
    val (shortcut, conflicts) = entry
wenzelm@63736
   102
    conflicts.foreach(s => keymap.setShortcut(s.property, ""))
wenzelm@63736
   103
    keymap.setShortcut(shortcut.property, shortcut.binding)
wenzelm@63736
   104
  }
wenzelm@63734
   105
wenzelm@63737
   106
  def get_shortcut_conflicts(keymap: Keymap): List[(Shortcut, List[Shortcut])] =
wenzelm@63734
   107
  {
wenzelm@63736
   108
    val keymap_shortcuts =
wenzelm@63736
   109
      if (keymap == null) Nil
wenzelm@63736
   110
      else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
wenzelm@63736
   111
wenzelm@63737
   112
    for (s <- convert_properties(jEdit.getProperties)) yield {
wenzelm@63736
   113
      val conflicts =
wenzelm@63736
   114
        keymap_shortcuts.filter(s1 =>
wenzelm@63736
   115
          s.property == s1.property && s.binding != s1.binding ||
wenzelm@63736
   116
          s.property != s1.property && s.binding == s1.binding)
wenzelm@63736
   117
      (s, conflicts)
wenzelm@63734
   118
    }
wenzelm@63734
   119
  }
wenzelm@63734
   120
wenzelm@63734
   121
wenzelm@63734
   122
wenzelm@63737
   123
  /** table model **/
wenzelm@63737
   124
wenzelm@63739
   125
  private def conflict_color: Color =
wenzelm@63739
   126
    PIDE.options.color_value("error_color")
wenzelm@63739
   127
wenzelm@63740
   128
  private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int])
wenzelm@63737
   129
  {
wenzelm@63738
   130
    override def toString: String =
wenzelm@63740
   131
      if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
wenzelm@63738
   132
      else
wenzelm@63739
   133
        "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
wenzelm@63739
   134
          HTML.output("--- " + shortcut.toString) +
wenzelm@63738
   135
        "</font></html>"
wenzelm@63737
   136
  }
wenzelm@63737
   137
wenzelm@63737
   138
  private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel
wenzelm@63737
   139
  {
wenzelm@63737
   140
    private val entries_count = entries.length
wenzelm@63737
   141
    private def get_entry(row: Int): Option[Table_Entry] =
wenzelm@63737
   142
      if (0 <= row && row <= entries_count) Some(entries(row)) else None
wenzelm@63737
   143
wenzelm@63740
   144
    private val selected =
wenzelm@63740
   145
      Synchronized[Set[Int]](
wenzelm@63740
   146
        (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
wenzelm@63737
   147
wenzelm@63737
   148
    def select(row: Int, b: Boolean)
wenzelm@63737
   149
    {
wenzelm@63740
   150
      if (get_entry(row).isDefined)
wenzelm@63740
   151
        selected.change(set => if (b) set + row else set - row)
wenzelm@63737
   152
    }
wenzelm@63737
   153
wenzelm@63737
   154
    def selected_status(row: Int): Option[Boolean] =
wenzelm@63740
   155
      if (get_entry(row).isDefined) Some(selected.value.contains(row)) else None
wenzelm@63737
   156
wenzelm@63737
   157
    override def getColumnCount: Int = 2
wenzelm@63737
   158
wenzelm@63737
   159
    override def getColumnClass(i: Int): Class[_ <: Object] =
wenzelm@63737
   160
      if (i == 0) classOf[java.lang.Boolean]
wenzelm@63737
   161
      else classOf[java.lang.Object]
wenzelm@63737
   162
wenzelm@63737
   163
    override def getColumnName(i: Int): String =
wenzelm@63737
   164
      if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???"
wenzelm@63737
   165
wenzelm@63737
   166
    override def getRowCount: Int = entries_count
wenzelm@63737
   167
wenzelm@63737
   168
    override def getValueAt(row: Int, column: Int): AnyRef =
wenzelm@63737
   169
    {
wenzelm@63737
   170
      get_entry(row) match {
wenzelm@63737
   171
        case Some(entry) if column == 0 =>
wenzelm@63737
   172
          selected_status(row) match {
wenzelm@63737
   173
            case None => null
wenzelm@63739
   174
            case Some(b) => java.lang.Boolean.valueOf(b)
wenzelm@63737
   175
          }
wenzelm@63738
   176
        case Some(entry) if column == 1 => entry
wenzelm@63737
   177
        case _ => null
wenzelm@63737
   178
      }
wenzelm@63737
   179
    }
wenzelm@63739
   180
wenzelm@63739
   181
    override def isCellEditable(row: Int, column: Int): Boolean =
wenzelm@63739
   182
      get_entry(row) match {
wenzelm@63740
   183
        case Some(entry) => column == 0
wenzelm@63739
   184
        case None => false
wenzelm@63739
   185
      }
wenzelm@63739
   186
wenzelm@63739
   187
    override def setValueAt(value: AnyRef, row: Int, column: Int)
wenzelm@63739
   188
    {
wenzelm@63739
   189
      (get_entry(row), value) match {
wenzelm@63740
   190
        case (Some(entry), obj: java.lang.Boolean) if entry.head.isEmpty && column == 0 =>
wenzelm@63740
   191
          val b = obj.booleanValue
wenzelm@63740
   192
          select(row, b)
wenzelm@63740
   193
          if (entry.tail.nonEmpty) {
wenzelm@63740
   194
            entry.tail.foreach(select(_, !b))
wenzelm@63740
   195
            GUI_Thread.later { fireTableDataChanged() }
wenzelm@63740
   196
          }
wenzelm@63739
   197
        case _ =>
wenzelm@63739
   198
      }
wenzelm@63739
   199
    }
wenzelm@63737
   200
  }
wenzelm@63737
   201
wenzelm@63737
   202
wenzelm@63737
   203
wenzelm@63734
   204
  /** dialog **/
wenzelm@63734
   205
wenzelm@63737
   206
  def check_dialog(view: View)
wenzelm@63734
   207
  {
wenzelm@63734
   208
    GUI_Thread.require {}
wenzelm@63737
   209
wenzelm@63737
   210
    val (keymap_name, keymap) = get_keymap()
wenzelm@63737
   211
    val shortcut_conflicts = get_shortcut_conflicts(keymap)
wenzelm@63737
   212
wenzelm@63737
   213
    val pending_conflicts =
wenzelm@63737
   214
      shortcut_conflicts.filter({ case (s, cs) => !s.is_ignored(keymap_name) && cs.nonEmpty })
wenzelm@63737
   215
    if (pending_conflicts.nonEmpty) new Dialog(view, pending_conflicts)
wenzelm@63737
   216
    // FIXME else silent change
wenzelm@63734
   217
  }
wenzelm@63734
   218
wenzelm@63737
   219
  private class Dialog(view: View, shortcut_conflicts: List[(Shortcut, List[Shortcut])])
wenzelm@63737
   220
    extends JDialog(view)
wenzelm@63734
   221
  {
wenzelm@63734
   222
    /* table */
wenzelm@63734
   223
wenzelm@63737
   224
    val table_entries =
wenzelm@63737
   225
      for {
wenzelm@63740
   226
        ((shortcut, conflicts), i) <- shortcut_conflicts zip
wenzelm@63740
   227
          shortcut_conflicts.scanLeft(0)({ case (i, (_, conflicts)) => i + 1 + conflicts.length })
wenzelm@63740
   228
        entry <-
wenzelm@63740
   229
          Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) ::
wenzelm@63740
   230
          conflicts.map(Table_Entry(_, Some(i), Nil))
wenzelm@63737
   231
      } yield entry
wenzelm@63734
   232
wenzelm@63737
   233
    val table_model = new Table_Model(table_entries)
wenzelm@63734
   234
wenzelm@63737
   235
    val table = new JTable(table_model)
wenzelm@63737
   236
    table.setShowGrid(false)
wenzelm@63737
   237
    table.setIntercellSpacing(new Dimension(0, 0))
wenzelm@63737
   238
    table.setRowHeight(GUIUtilities.defaultRowHeight() + 2)
wenzelm@63737
   239
    table.setPreferredScrollableViewportSize(new Dimension(500, 300))
wenzelm@63737
   240
    table.getTableHeader.setReorderingAllowed(false)
wenzelm@63734
   241
wenzelm@63737
   242
		val col0 = table.getColumnModel.getColumn(0)
wenzelm@63737
   243
		val col1 = table.getColumnModel.getColumn(1)
wenzelm@63734
   244
wenzelm@63737
   245
		col0.setPreferredWidth(30)
wenzelm@63737
   246
		col0.setMinWidth(30)
wenzelm@63737
   247
		col0.setMaxWidth(30)
wenzelm@63737
   248
		col0.setResizable(false)
wenzelm@63734
   249
wenzelm@63737
   250
		col1.setPreferredWidth(300)
wenzelm@63734
   251
wenzelm@63734
   252
    val table_scroller = new JScrollPane(table)
wenzelm@63737
   253
		table_scroller.getViewport.setBackground(table.getBackground)
wenzelm@63737
   254
		table_scroller.setPreferredSize(new Dimension(400, 400))
wenzelm@63734
   255
wenzelm@63734
   256
wenzelm@63734
   257
    /* buttons */
wenzelm@63734
   258
wenzelm@63734
   259
    val ok_button = new Button("OK") {
wenzelm@63734
   260
      reactions += { case ButtonClicked(_) => close() }  // FIXME
wenzelm@63734
   261
    }
wenzelm@63734
   262
wenzelm@63734
   263
    val cancel_button = new Button("Cancel") {
wenzelm@63734
   264
      reactions += { case ButtonClicked(_) => close() }  // FIXME
wenzelm@63734
   265
    }
wenzelm@63734
   266
wenzelm@63734
   267
    private def close()
wenzelm@63734
   268
    {
wenzelm@63734
   269
      setVisible(false)
wenzelm@63734
   270
      dispose()
wenzelm@63734
   271
    }
wenzelm@63734
   272
wenzelm@63734
   273
wenzelm@63734
   274
    /* layout */
wenzelm@63734
   275
wenzelm@63734
   276
    private val action_panel = new FlowPanel(FlowPanel.Alignment.Right)(ok_button, cancel_button)
wenzelm@63734
   277
    private val layout_panel = new BorderPanel
wenzelm@63734
   278
    layout_panel.layout(Component.wrap(table_scroller)) = BorderPanel.Position.Center
wenzelm@63734
   279
    layout_panel.layout(action_panel) = BorderPanel.Position.South
wenzelm@63734
   280
wenzelm@63734
   281
    setContentPane(layout_panel.peer)
wenzelm@63734
   282
wenzelm@63734
   283
wenzelm@63734
   284
    /* main */
wenzelm@63734
   285
wenzelm@63734
   286
    setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE)
wenzelm@63734
   287
wenzelm@63734
   288
    setTitle("Isabelle/jEdit keymap changes")
wenzelm@63734
   289
wenzelm@63734
   290
    pack()
wenzelm@63734
   291
    setLocationRelativeTo(view)
wenzelm@63734
   292
    setVisible(true)
wenzelm@63734
   293
  }
wenzelm@63734
   294
}