# HG changeset patch
# User wenzelm
# Date 1472721687 -7200
# Node ID 10c08a4d39dd7b7752f3b8a80284110cdbb1b0e7
# Parent  7b2963b11e4a7d8b288385bc1ab2e4c471522047
tuned GUI;

diff -r 7b2963b11e4a -r 10c08a4d39dd src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Wed Aug 31 21:25:54 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 11:21:27 2016 +0200
@@ -232,11 +232,15 @@
 
     val table_model = new Table_Model(table_entries)
 
+    val cell_size = GUIUtilities.defaultTableCellSize()
+    val table_size = new Dimension(cell_size.width * 2, cell_size.height * 20)
+
     val table = new JTable(table_model)
     table.setShowGrid(false)
     table.setIntercellSpacing(new Dimension(0, 0))
-    table.setRowHeight(GUIUtilities.defaultRowHeight() + 2)
-    table.setPreferredScrollableViewportSize(new Dimension(500, 300))
+    table.setRowHeight(cell_size.height + 2)
+    table.setPreferredScrollableViewportSize(table_size)
+    table.setFillsViewportHeight(true)
     table.getTableHeader.setReorderingAllowed(false)
 
 		val col0 = table.getColumnModel.getColumn(0)
@@ -247,11 +251,11 @@
 		col0.setMaxWidth(30)
 		col0.setResizable(false)
 
-		col1.setPreferredWidth(300)
+		col1.setPreferredWidth(table_size.width)
 
     val table_scroller = new JScrollPane(table)
 		table_scroller.getViewport.setBackground(table.getBackground)
-		table_scroller.setPreferredSize(new Dimension(400, 400))
+		table_scroller.setPreferredSize(table_size)
 
 
     /* buttons */