15 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel} |
15 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel} |
16 |
16 |
17 import org.gjt.sp.jedit.{View, OperatingSystem} |
17 import org.gjt.sp.jedit.{View, OperatingSystem} |
18 |
18 |
19 |
19 |
20 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) |
20 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) { |
21 { |
|
22 private val doc_contents = Doc.contents() |
21 private val doc_contents = Doc.contents() |
23 |
22 |
24 private case class Node(string: String, entry: Doc.Entry) |
23 private case class Node(string: String, entry: Doc.Entry) { |
25 { |
|
26 override def toString: String = string |
24 override def toString: String = string |
27 } |
25 } |
28 |
26 |
29 private val root = new DefaultMutableTreeNode |
27 private val root = new DefaultMutableTreeNode |
30 for (section <- doc_contents.sections) { |
28 for (section <- doc_contents.sections) { |
45 tree.setRowHeight(0) |
43 tree.setRowHeight(0) |
46 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
44 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
47 |
45 |
48 override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow |
46 override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow |
49 |
47 |
50 private def action(node: DefaultMutableTreeNode): Unit = |
48 private def action(node: DefaultMutableTreeNode): Unit = { |
51 { |
|
52 node.getUserObject match { |
49 node.getUserObject match { |
53 case Node(_, Doc.Doc(_, _, path)) => |
50 case Node(_, Doc.Doc(_, _, path)) => |
54 PIDE.editor.goto_doc(view, path) |
51 PIDE.editor.goto_doc(view, path) |
55 case Node(_, Doc.Text_File(_, path)) => |
52 case Node(_, Doc.Text_File(_, path)) => |
56 PIDE.editor.goto_file(true, view, File.platform_path(path)) |
53 PIDE.editor.goto_file(true, view, File.platform_path(path)) |
57 case _ => |
54 case _ => |
58 } |
55 } |
59 } |
56 } |
60 |
57 |
61 tree.addKeyListener(new KeyAdapter { |
58 tree.addKeyListener(new KeyAdapter { |
62 override def keyPressed(e: KeyEvent): Unit = |
59 override def keyPressed(e: KeyEvent): Unit = { |
63 { |
|
64 if (e.getKeyCode == KeyEvent.VK_ENTER) { |
60 if (e.getKeyCode == KeyEvent.VK_ENTER) { |
65 e.consume |
61 e.consume |
66 val path = tree.getSelectionPath |
62 val path = tree.getSelectionPath |
67 if (path != null) { |
63 if (path != null) { |
68 path.getLastPathComponent match { |
64 path.getLastPathComponent match { |
72 } |
68 } |
73 } |
69 } |
74 } |
70 } |
75 }) |
71 }) |
76 tree.addMouseListener(new MouseAdapter { |
72 tree.addMouseListener(new MouseAdapter { |
77 override def mouseClicked(e: MouseEvent): Unit = |
73 override def mouseClicked(e: MouseEvent): Unit = { |
78 { |
|
79 val click = tree.getPathForLocation(e.getX, e.getY) |
74 val click = tree.getPathForLocation(e.getX, e.getY) |
80 if (click != null && e.getClickCount == 1) { |
75 if (click != null && e.getClickCount == 1) { |
81 (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { |
76 (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { |
82 case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 => |
77 case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 => |
83 action(node) |
78 action(node) |