5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 import javax.swing.JTree |
9 import javax.swing.JTree |
10 import javax.swing.tree.{MutableTreeNode, TreeSelectionModel} |
10 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel} |
11 |
11 |
12 |
12 |
13 class Tree_View(root: MutableTreeNode, single_selection_mode: Boolean = false) extends JTree(root) { |
13 class Tree_View( |
14 tree => |
14 val root: DefaultMutableTreeNode = new DefaultMutableTreeNode, |
|
15 single_selection_mode: Boolean = false |
|
16 ) extends JTree(root) { |
|
17 def get_selection[A](which: PartialFunction[AnyRef, A]): Option[A] = |
|
18 getLastSelectedPathComponent match { |
|
19 case node: DefaultMutableTreeNode => |
|
20 val obj = node.getUserObject |
|
21 if (obj != null && which.isDefinedAt(obj)) Some(which(obj)) |
|
22 else None |
|
23 case _ => None |
|
24 } |
15 |
25 |
16 tree.setRowHeight(0) |
26 def clear(): Unit = { |
|
27 clearSelection() |
|
28 root.removeAllChildren() |
|
29 } |
|
30 |
|
31 def reload_model(): Unit = |
|
32 getModel.asInstanceOf[DefaultTreeModel].reload(root) |
|
33 |
|
34 |
|
35 /* init */ |
|
36 |
|
37 setRowHeight(0) |
17 |
38 |
18 if (single_selection_mode) { |
39 if (single_selection_mode) { |
19 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
40 getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
20 } |
41 } |
21 |
42 |
22 // follow jEdit |
43 // follow jEdit |
23 if (!GUI.is_macos_laf) { |
44 if (!GUI.is_macos_laf) { |
24 tree.putClientProperty("JTree.lineStyle", "Angled") |
45 putClientProperty("JTree.lineStyle", "Angled") |
25 } |
46 } |
26 } |
47 } |