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