equal
deleted
inserted
replaced
68 |
68 |
69 private var nodes = List.empty[Graph_Display.Node] |
69 private var nodes = List.empty[Graph_Display.Node] |
70 private val root = new DefaultMutableTreeNode("Nodes") |
70 private val root = new DefaultMutableTreeNode("Nodes") |
71 |
71 |
72 val tree = new JTree(root) |
72 val tree = new JTree(root) |
|
73 tree.setRowHeight(0) |
73 |
74 |
74 tree.addKeyListener(new KeyAdapter { |
75 tree.addKeyListener(new KeyAdapter { |
75 override def keyPressed(e: KeyEvent): Unit = |
76 override def keyPressed(e: KeyEvent): Unit = |
76 if (e.getKeyCode == KeyEvent.VK_ENTER) { |
77 if (e.getKeyCode == KeyEvent.VK_ENTER) { |
77 e.consume |
78 e.consume |