src/Tools/jEdit/src/documentation_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62113 16de2a9b5b3d
child 65246 848965b5befc
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/documentation_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for Isabelle documentation.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.Dimension
    13 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
    14 import javax.swing.{JTree, JScrollPane}
    15 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
    16 
    17 import org.gjt.sp.jedit.{View, OperatingSystem}
    18 
    19 
    20 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
    21 {
    22   private val docs = Doc.contents()
    23 
    24   private case class Documentation(name: String, title: String, path: Path)
    25   {
    26     override def toString: String =
    27       "<html><b>" + HTML.output(name) + "</b>:  " + HTML.output(title) + "</html>"
    28   }
    29 
    30   private case class Text_File(name: String, path: Path)
    31   {
    32     override def toString: String = name
    33   }
    34 
    35   private val root = new DefaultMutableTreeNode
    36   docs foreach {
    37     case Doc.Section(text, _) =>
    38       root.add(new DefaultMutableTreeNode(text))
    39     case Doc.Doc(name, title, path) =>
    40       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    41         .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
    42     case Doc.Text_File(name: String, path: Path) =>
    43       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    44         .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
    45   }
    46 
    47   private val tree = new JTree(root)
    48   tree.setRowHeight(0)
    49   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
    50 
    51   override def focusOnDefaultComponent { tree.requestFocusInWindow }
    52 
    53   private def action(node: DefaultMutableTreeNode)
    54   {
    55     node.getUserObject match {
    56       case Text_File(_, path) =>
    57         PIDE.editor.goto_file(true, view, File.platform_path(path))
    58       case Documentation(_, _, path) =>
    59         PIDE.editor.goto_doc(view, path)
    60       case _ =>
    61     }
    62   }
    63 
    64   tree.addKeyListener(new KeyAdapter {
    65     override def keyPressed(e: KeyEvent)
    66     {
    67       if (e.getKeyCode == KeyEvent.VK_ENTER) {
    68         e.consume
    69         val path = tree.getSelectionPath
    70         if (path != null) {
    71           path.getLastPathComponent match {
    72             case node: DefaultMutableTreeNode => action(node)
    73             case _ =>
    74           }
    75         }
    76       }
    77     }
    78   })
    79   tree.addMouseListener(new MouseAdapter {
    80     override def mouseClicked(e: MouseEvent)
    81     {
    82       val click = tree.getPathForLocation(e.getX, e.getY)
    83       if (click != null && e.getClickCount == 1) {
    84         (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
    85           case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
    86             action(node)
    87           case _ =>
    88         }
    89       }
    90     }
    91   })
    92 
    93   {
    94     var expand = true
    95     var visible = 0
    96     def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
    97     for ((entry, row) <- docs.zipWithIndex) {
    98       entry match {
    99         case Doc.Section(_, important) =>
   100           expand = important
   101           make_visible(row)
   102         case _ =>
   103           if (expand) make_visible(row)
   104       }
   105     }
   106     tree.setRootVisible(false)
   107     tree.setVisibleRowCount(visible)
   108   }
   109 
   110   private val tree_view = new JScrollPane(tree)
   111   tree_view.setMinimumSize(new Dimension(200, 50))
   112 
   113   set_content(tree_view)
   114 }