isabelle: src/Tools/jEdit/src/keymap_merge.scala@352a257fa13a (annotated)

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

author	wenzelm
	Wed, 31 Aug 2016 20:35:15 +0200
changeset 63739	352a257fa13a
parent 63738	f215f5f5bd35
child 63740	7b2963b11e4a
permissions	-rw-r--r--