wenzelm@63734: /* Title: Tools/jEdit/src/keymap_merge.scala wenzelm@63734: Author: Makarius wenzelm@63734: wenzelm@63736: Merge of Isabelle shortcuts vs. jEdit keymap. wenzelm@63734: */ wenzelm@63734: wenzelm@63734: package isabelle.jedit wenzelm@63734: wenzelm@63734: wenzelm@63734: import isabelle._ wenzelm@63734: wenzelm@63743: import java.lang.{Class, Boolean => JBoolean} wenzelm@63745: import java.awt.{Color, Dimension, BorderLayout} wenzelm@63745: import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane} wenzelm@63737: import javax.swing.table.AbstractTableModel wenzelm@63734: wenzelm@63734: import scala.collection.JavaConversions wenzelm@63734: wenzelm@63748: import org.gjt.sp.jedit.{jEdit, View, GUIUtilities} wenzelm@63734: import org.jedit.keymap.{KeymapManager, Keymap} wenzelm@63734: wenzelm@63734: wenzelm@63734: object Keymap_Merge wenzelm@63734: { wenzelm@63736: /** shortcuts **/ wenzelm@63734: wenzelm@63736: private def is_shortcut(property: String): Boolean = wenzelm@63736: (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && wenzelm@63736: !property.startsWith("options.shortcuts.") wenzelm@63736: wenzelm@63736: class Shortcut(val property: String, val binding: String) wenzelm@63734: { wenzelm@63736: override def toString: String = property + "=" + binding wenzelm@63736: wenzelm@63736: def primary: Boolean = property.endsWith(".shortcut") wenzelm@63734: wenzelm@63736: val action: String = wenzelm@63736: Library.try_unsuffix(".shortcut", property) orElse wenzelm@63736: Library.try_unsuffix(".shortcut2", property) getOrElse wenzelm@63736: error("Bad shortcut property: " + quote(property)) wenzelm@63736: wenzelm@63734: val label: String = wenzelm@63734: GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) wenzelm@63736: wenzelm@63736: wenzelm@63745: /* ignore wrt. keymap */ wenzelm@63736: wenzelm@63736: private def prop_ignore: String = property + ".ignore" wenzelm@63736: wenzelm@63736: def ignored_keymaps(): List[String] = wenzelm@63736: Library.space_explode(',', jEdit.getProperty(prop_ignore, "")) wenzelm@63736: wenzelm@63736: def is_ignored(keymap_name: String): Boolean = wenzelm@63736: ignored_keymaps().contains(keymap_name) wenzelm@63736: wenzelm@63772: def ignore(keymap_name: String): Unit = wenzelm@63772: jEdit.setProperty(prop_ignore, wenzelm@63772: Library.insert(keymap_name)(ignored_keymaps()).sorted.mkString(",")) wenzelm@63745: wenzelm@63745: def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding) wenzelm@63745: def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null) wenzelm@63734: } wenzelm@63734: wenzelm@63745: wenzelm@63745: /* content wrt. keymap */ wenzelm@63745: wenzelm@63736: def convert_properties(props: java.util.Properties): List[Shortcut] = wenzelm@63736: if (props == null) Nil wenzelm@63736: else { wenzelm@63736: var result = List.empty[Shortcut] wenzelm@63736: for (entry <- JavaConversions.mapAsScalaMap(props)) { wenzelm@63736: entry match { wenzelm@63736: case (a: String, b: String) if is_shortcut(a) => wenzelm@63736: result ::= new Shortcut(a, b) wenzelm@63736: case _ => wenzelm@63736: } wenzelm@63736: } wenzelm@63736: result.sortBy(_.property) wenzelm@63736: } wenzelm@63736: wenzelm@63745: def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] = wenzelm@63734: { wenzelm@63736: val keymap_shortcuts = wenzelm@63736: if (keymap == null) Nil wenzelm@63736: else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) wenzelm@63736: wenzelm@63745: for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield { wenzelm@63736: val conflicts = wenzelm@63736: keymap_shortcuts.filter(s1 => wenzelm@63736: s.property == s1.property && s.binding != s1.binding || wenzelm@63742: s.property != s1.property && s.binding == s1.binding && s1.binding != "") wenzelm@63736: (s, conflicts) wenzelm@63734: } wenzelm@63734: } wenzelm@63734: wenzelm@63734: wenzelm@63734: wenzelm@63745: /** table **/ wenzelm@63737: wenzelm@63739: private def conflict_color: Color = wenzelm@63739: PIDE.options.color_value("error_color") wenzelm@63739: wenzelm@63740: private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) wenzelm@63737: { wenzelm@63738: override def toString: String = wenzelm@63740: if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" wenzelm@63738: else wenzelm@63739: "" + wenzelm@63739: HTML.output("--- " + shortcut.toString) + wenzelm@63738: "" wenzelm@63737: } wenzelm@63737: wenzelm@63737: private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel wenzelm@63737: { wenzelm@63737: private val entries_count = entries.length wenzelm@63743: private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count wenzelm@63737: private def get_entry(row: Int): Option[Table_Entry] = wenzelm@63743: if (has_entry(row)) Some(entries(row)) else None wenzelm@63737: wenzelm@63740: private val selected = wenzelm@63740: Synchronized[Set[Int]]( wenzelm@63740: (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet) wenzelm@63737: wenzelm@63745: private def is_selected(row: Int): Boolean = wenzelm@63745: selected.value.contains(row) wenzelm@63744: wenzelm@63745: private def select(head: Int, tail: List[Int], b: Boolean): Unit = wenzelm@63743: selected.change(set => if (b) set + head -- tail else set - head ++ tail) wenzelm@63737: wenzelm@63744: def apply(keymap_name: String, keymap: Keymap) wenzelm@63744: { wenzelm@63744: GUI_Thread.require {} wenzelm@63744: wenzelm@63744: for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { wenzelm@63744: val b = is_selected(row) wenzelm@63744: if (b) { wenzelm@63745: entry.tail.foreach(i => entries(i).shortcut.reset(keymap)) wenzelm@63745: entry.shortcut.set(keymap) wenzelm@63744: } wenzelm@63750: else wenzelm@63750: entry.shortcut.ignore(keymap_name) wenzelm@63744: } wenzelm@63744: } wenzelm@63744: wenzelm@63737: override def getColumnCount: Int = 2 wenzelm@63737: wenzelm@63737: override def getColumnClass(i: Int): Class[_ <: Object] = wenzelm@63743: if (i == 0) classOf[JBoolean] else classOf[Object] wenzelm@63737: wenzelm@63737: override def getColumnName(i: Int): String = wenzelm@63737: if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" wenzelm@63737: wenzelm@63737: override def getRowCount: Int = entries_count wenzelm@63737: wenzelm@63737: override def getValueAt(row: Int, column: Int): AnyRef = wenzelm@63737: { wenzelm@63737: get_entry(row) match { wenzelm@63744: case Some(entry) if column == 0 => JBoolean.valueOf(is_selected(row)) wenzelm@63738: case Some(entry) if column == 1 => entry wenzelm@63737: case _ => null wenzelm@63737: } wenzelm@63737: } wenzelm@63739: wenzelm@63739: override def isCellEditable(row: Int, column: Int): Boolean = wenzelm@63743: has_entry(row) && column == 0 wenzelm@63739: wenzelm@63739: override def setValueAt(value: AnyRef, row: Int, column: Int) wenzelm@63739: { wenzelm@63743: value match { wenzelm@63743: case obj: JBoolean if has_entry(row) && column == 0 => wenzelm@63740: val b = obj.booleanValue wenzelm@63743: val entry = entries(row) wenzelm@63743: entry.head match { wenzelm@63743: case None => select(row, entry.tail, b) wenzelm@63743: case Some(head_row) => wenzelm@63743: val head_entry = entries(head_row) wenzelm@63743: select(head_row, head_entry.tail, !b) wenzelm@63740: } wenzelm@63743: GUI_Thread.later { fireTableDataChanged() } wenzelm@63739: case _ => wenzelm@63739: } wenzelm@63739: } wenzelm@63737: } wenzelm@63737: wenzelm@63745: private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) wenzelm@63734: { wenzelm@63745: private val cell_size = GUIUtilities.defaultTableCellSize() wenzelm@63745: private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) wenzelm@63741: wenzelm@63737: val table = new JTable(table_model) wenzelm@63737: table.setShowGrid(false) wenzelm@63737: table.setIntercellSpacing(new Dimension(0, 0)) wenzelm@63741: table.setRowHeight(cell_size.height + 2) wenzelm@63741: table.setPreferredScrollableViewportSize(table_size) wenzelm@63741: table.setFillsViewportHeight(true) wenzelm@63737: table.getTableHeader.setReorderingAllowed(false) wenzelm@63734: wenzelm@63745: table.getColumnModel.getColumn(0).setPreferredWidth(30) wenzelm@63745: table.getColumnModel.getColumn(0).setMinWidth(30) wenzelm@63745: table.getColumnModel.getColumn(0).setMaxWidth(30) wenzelm@63745: table.getColumnModel.getColumn(0).setResizable(false) wenzelm@63745: table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30) wenzelm@63734: wenzelm@63745: val scroller = new JScrollPane(table) wenzelm@63745: scroller.getViewport.setBackground(table.getBackground) wenzelm@63745: scroller.setPreferredSize(table_size) wenzelm@63734: wenzelm@63745: add(scroller, BorderLayout.CENTER) wenzelm@63745: } wenzelm@63734: wenzelm@63734: wenzelm@63734: wenzelm@63745: /** check with optional dialog **/ wenzelm@63745: wenzelm@63748: def check_dialog(view: View) wenzelm@63745: { wenzelm@63745: GUI_Thread.require {} wenzelm@63745: wenzelm@63745: val keymap_manager = jEdit.getKeymapManager wenzelm@63745: val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) wenzelm@63745: val keymap = wenzelm@63745: keymap_manager.getKeymap(keymap_name) match { wenzelm@63745: case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) wenzelm@63745: case keymap => keymap wenzelm@63745: } wenzelm@63745: wenzelm@63745: val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap) wenzelm@63745: val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s wenzelm@63745: val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty) wenzelm@63734: wenzelm@63745: val table_entries = wenzelm@63745: for { wenzelm@63745: ((shortcut, conflicts), i) <- shortcut_conflicts zip wenzelm@63745: shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length }) wenzelm@63745: entry <- wenzelm@63745: Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: wenzelm@63745: conflicts.map(Table_Entry(_, Some(i), Nil)) wenzelm@63745: } yield entry wenzelm@63745: wenzelm@63745: val table_model = new Table_Model(table_entries) wenzelm@63734: wenzelm@63745: if (table_entries.nonEmpty && wenzelm@63748: GUI.confirm_dialog(view, wenzelm@63745: "Pending Isabelle/jEdit keymap changes", wenzelm@63745: JOptionPane.OK_CANCEL_OPTION, wenzelm@63753: "The following Isabelle keymap changes are in conflict with the current", wenzelm@63759: "jEdit keymap " + quote(keymap_name) + ":", wenzelm@63745: new Table(table_model), wenzelm@63748: "Selected shortcuts will be applied, unselected changes will be ignored.", wenzelm@63753: "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0) wenzelm@63750: { table_model.apply(keymap_name, keymap) } wenzelm@63750: wenzelm@63750: no_shortcut_conflicts.foreach(_.set(keymap)) wenzelm@63734: wenzelm@63750: keymap.save() wenzelm@63750: keymap_manager.reload() wenzelm@63750: jEdit.saveSettings() wenzelm@63734: } wenzelm@63734: }