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