Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace;
authorwenzelm
Fri, 18 Feb 2022 15:07:43 +0100
changeset 75097 7001ae6c0832
parent 75096 37bd912c8765
child 75098 9e79c9f55edd
tuned whitespace;
src/Tools/jEdit/src/keymap_merge.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/keymap_merge.scala	Fri Feb 18 14:03:45 2022 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Fri Feb 18 15:07:43 2022 +0100
@@ -196,15 +196,15 @@
     table.setFillsViewportHeight(true)
     table.getTableHeader.setReorderingAllowed(false)
 
-		table.getColumnModel.getColumn(0).setPreferredWidth(30)
-		table.getColumnModel.getColumn(0).setMinWidth(30)
-		table.getColumnModel.getColumn(0).setMaxWidth(30)
-		table.getColumnModel.getColumn(0).setResizable(false)
-		table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
+    table.getColumnModel.getColumn(0).setPreferredWidth(30)
+    table.getColumnModel.getColumn(0).setMinWidth(30)
+    table.getColumnModel.getColumn(0).setMaxWidth(30)
+    table.getColumnModel.getColumn(0).setResizable(false)
+    table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
 
     val scroller = new JScrollPane(table)
-		scroller.getViewport.setBackground(table.getBackground)
-		scroller.setPreferredSize(table_size)
+    scroller.getViewport.setBackground(table.getBackground)
+    scroller.setPreferredSize(table_size)
 
     add(scroller, BorderLayout.CENTER)
   }
isabelle