src/Tools/jEdit/src/keymap_merge.scala
author wenzelm
Tue Aug 30 21:56:14 2016 +0200 (2016-08-30)
changeset 63734 133e3e84e6fb
child 63736 33fb64d7842a
permissions -rw-r--r--
some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm@63734
     1
/*  Title:      Tools/jEdit/src/keymap_merge.scala
wenzelm@63734
     2
    Author:     Makarius
wenzelm@63734
     3
wenzelm@63734
     4
Merge of Isabelle/jEdit shortcuts wrt. 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.mutable
wenzelm@63734
    16
import scala.collection.JavaConversions
wenzelm@63734
    17
import scala.collection.immutable.SortedSet
wenzelm@63734
    18
import scala.swing.{FlowPanel, BorderPanel, Component, Button}
wenzelm@63734
    19
import scala.swing.event.ButtonClicked
wenzelm@63734
    20
wenzelm@63734
    21
import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
wenzelm@63734
    22
import org.jedit.keymap.{KeymapManager, Keymap}
wenzelm@63734
    23
wenzelm@63734
    24
wenzelm@63734
    25
object Keymap_Merge
wenzelm@63734
    26
{
wenzelm@63734
    27
  /* Isabelle/jEdit shortcuts */
wenzelm@63734
    28
wenzelm@63734
    29
  sealed case class Shortcut(action: String, key: String, alternative: Boolean)
wenzelm@63734
    30
  {
wenzelm@63734
    31
    def eq_action(that: Shortcut): Boolean = action == that.action
wenzelm@63734
    32
wenzelm@63734
    33
    val property: String = if (alternative) action + ".shortcut2" else action + ".shortcut"
wenzelm@63734
    34
    val label: String =
wenzelm@63734
    35
      GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
wenzelm@63734
    36
  }
wenzelm@63734
    37
wenzelm@63734
    38
  def additional_shortcuts(): List[Shortcut] =
wenzelm@63734
    39
  {
wenzelm@63734
    40
    val result = new mutable.ListBuffer[Shortcut]
wenzelm@63734
    41
    for (entry <- JavaConversions.mapAsScalaMap(jEdit.getProperties)) {
wenzelm@63734
    42
      entry match {
wenzelm@63734
    43
        case (a: String, b: String) if a.endsWith(".shortcut") =>
wenzelm@63734
    44
          val action = a.substring(0, a.length - 9)
wenzelm@63734
    45
          result += Shortcut(action, b, false)
wenzelm@63734
    46
        case (a: String, b: String) if a.endsWith(".shortcut2") =>
wenzelm@63734
    47
          val action = a.substring(0, a.length - 10)
wenzelm@63734
    48
          result += Shortcut(action, b, true)
wenzelm@63734
    49
        case _ =>
wenzelm@63734
    50
      }
wenzelm@63734
    51
    }
wenzelm@63734
    52
    result.toList
wenzelm@63734
    53
  }
wenzelm@63734
    54
wenzelm@63734
    55
wenzelm@63734
    56
  /* jEdit keymap */
wenzelm@63734
    57
wenzelm@63734
    58
  def current_keymap(): Keymap =
wenzelm@63734
    59
  {
wenzelm@63734
    60
    val manager = jEdit.getKeymapManager
wenzelm@63734
    61
    val name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63734
    62
    manager.getKeymap(name) match {
wenzelm@63734
    63
      case null => manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
wenzelm@63734
    64
      case keymap => keymap
wenzelm@63734
    65
    }
wenzelm@63734
    66
  }
wenzelm@63734
    67
wenzelm@63734
    68
wenzelm@63734
    69
wenzelm@63734
    70
  /** dialog **/
wenzelm@63734
    71
wenzelm@63734
    72
  def dialog(view: View)
wenzelm@63734
    73
  {
wenzelm@63734
    74
    GUI_Thread.require {}
wenzelm@63734
    75
    new Dialog(view)
wenzelm@63734
    76
  }
wenzelm@63734
    77
wenzelm@63734
    78
  private class Dialog(view: View) extends JDialog(view)
wenzelm@63734
    79
  {
wenzelm@63734
    80
    /* table */
wenzelm@63734
    81
wenzelm@63734
    82
    val shortcuts = additional_shortcuts()
wenzelm@63734
    83
wenzelm@63734
    84
    def get_label(action: String): String =
wenzelm@63734
    85
      shortcuts.collectFirst(
wenzelm@63734
    86
        { case s if s.action == action && s.label != "" => s.label }).getOrElse(action)
wenzelm@63734
    87
wenzelm@63734
    88
    def get_key(action: String, alternative: Boolean): String =
wenzelm@63734
    89
      shortcuts.collectFirst(
wenzelm@63734
    90
        { case s if s.action == action && s.alternative == alternative => s.key }).getOrElse("")
wenzelm@63734
    91
wenzelm@63734
    92
    val column_names: Array[AnyRef] =
wenzelm@63734
    93
      Array(jEdit.getProperty("options.shortcuts.name"),
wenzelm@63734
    94
        jEdit.getProperty("options.shortcuts.shortcut1"),
wenzelm@63734
    95
        jEdit.getProperty("options.shortcuts.shortcut2"))
wenzelm@63734
    96
wenzelm@63734
    97
    val table_rows: Array[Array[AnyRef]] =
wenzelm@63734
    98
      Library.distinct[Shortcut](shortcuts, _ eq_action _).sortBy(_.action).
wenzelm@63734
    99
        map(s => Array[AnyRef](s.label, get_key(s.action, false), get_key(s.action, true))).toArray
wenzelm@63734
   100
wenzelm@63734
   101
    val table = new JTable(table_rows, column_names)
wenzelm@63734
   102
    table.setRowHeight(GUIUtilities.defaultRowHeight())
wenzelm@63734
   103
    table.getTableHeader().setReorderingAllowed(false)  // FIXME !?
wenzelm@63734
   104
wenzelm@63734
   105
    val table_size = table.getPreferredSize()
wenzelm@63734
   106
    table_size.height = table_size.height min 200
wenzelm@63734
   107
wenzelm@63734
   108
    val table_scroller = new JScrollPane(table)
wenzelm@63734
   109
    table_scroller.setPreferredSize(table_size)
wenzelm@63734
   110
wenzelm@63734
   111
wenzelm@63734
   112
    /* buttons */
wenzelm@63734
   113
wenzelm@63734
   114
    val ok_button = new Button("OK") {
wenzelm@63734
   115
      reactions += { case ButtonClicked(_) => close() }  // FIXME
wenzelm@63734
   116
    }
wenzelm@63734
   117
wenzelm@63734
   118
    val cancel_button = new Button("Cancel") {
wenzelm@63734
   119
      reactions += { case ButtonClicked(_) => close() }  // FIXME
wenzelm@63734
   120
    }
wenzelm@63734
   121
wenzelm@63734
   122
    private def close()
wenzelm@63734
   123
    {
wenzelm@63734
   124
      setVisible(false)
wenzelm@63734
   125
      dispose()
wenzelm@63734
   126
    }
wenzelm@63734
   127
wenzelm@63734
   128
wenzelm@63734
   129
    /* layout */
wenzelm@63734
   130
wenzelm@63734
   131
    private val action_panel = new FlowPanel(FlowPanel.Alignment.Right)(ok_button, cancel_button)
wenzelm@63734
   132
    private val layout_panel = new BorderPanel
wenzelm@63734
   133
    layout_panel.layout(Component.wrap(table_scroller)) = BorderPanel.Position.Center
wenzelm@63734
   134
    layout_panel.layout(action_panel) = BorderPanel.Position.South
wenzelm@63734
   135
wenzelm@63734
   136
    setContentPane(layout_panel.peer)
wenzelm@63734
   137
wenzelm@63734
   138
wenzelm@63734
   139
    /* main */
wenzelm@63734
   140
wenzelm@63734
   141
    setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE)
wenzelm@63734
   142
wenzelm@63734
   143
    setTitle("Isabelle/jEdit keymap changes")
wenzelm@63734
   144
wenzelm@63734
   145
    pack()
wenzelm@63734
   146
    setLocationRelativeTo(view)
wenzelm@63734
   147
    setVisible(true)
wenzelm@63734
   148
  }
wenzelm@63734
   149
}