src/Pure/GUI/tree_view.scala
changeset 81325 458e9e3b356e
parent 81323 33fbf90fbc1d
child 81326 403203217493
equal deleted inserted replaced
81324:0ec5131899b6 81325:458e9e3b356e
     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 }