tuned GUI;
authorwenzelm
Thu, 01 Sep 2016 11:21:27 +0200
changeset 63743 10c08a4d39dd
parent 63742 7b2963b11e4a
child 63744 1e676fcd7ede
tuned GUI;
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 */