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 { |
21 { |
22 private val docs = Doc.contents() |
22 private val sections = Doc.contents() |
23 |
23 |
24 private case class Documentation(name: String, title: String, path: Path) |
24 private case class Documentation(name: String, title: String, path: Path) |
25 { |
25 { |
26 override def toString: String = |
26 override def toString: String = |
27 "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" |
27 "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" |
31 { |
31 { |
32 override def toString: String = name |
32 override def toString: String = name |
33 } |
33 } |
34 |
34 |
35 private val root = new DefaultMutableTreeNode |
35 private val root = new DefaultMutableTreeNode |
36 docs foreach { |
36 for (section <- sections) { |
37 case Doc.Heading(text, _) => |
37 root.add(new DefaultMutableTreeNode(section.title)) |
38 root.add(new DefaultMutableTreeNode(text)) |
38 section.entries.foreach( |
39 case Doc.Doc(name, title, path) => |
39 { |
40 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
40 case Doc.Doc(name, title, path) => |
41 .add(new DefaultMutableTreeNode(Documentation(name, title, path))) |
41 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
42 case Doc.Text_File(name: String, path: Path) => |
42 .add(new DefaultMutableTreeNode(Documentation(name, title, path))) |
43 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
43 case Doc.Text_File(name: String, path: Path) => |
44 .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) |
44 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
|
45 .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) |
|
46 }) |
45 } |
47 } |
46 |
48 |
47 private val tree = new JTree(root) |
49 private val tree = new JTree(root) |
48 tree.setRowHeight(0) |
50 tree.setRowHeight(0) |
49 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
51 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
91 }) |
93 }) |
92 |
94 |
93 { |
95 { |
94 var expand = true |
96 var expand = true |
95 var visible = 0 |
97 var visible = 0 |
96 def make_visible(row: Int): Unit = { visible += 1; tree.expandRow(row) } |
98 var row = 0 |
97 for ((entry, row) <- docs.zipWithIndex) { |
99 def make_visible(): Unit = { visible += 1; tree.expandRow(row) } |
98 entry match { |
100 for (section <- sections) { |
99 case Doc.Heading(_, important) => |
101 expand = section.important |
100 expand = important |
102 make_visible() |
101 make_visible(row) |
103 row += 1 |
102 case _ => |
104 for (_ <- section.entries) { |
103 if (expand) make_visible(row) |
105 if (expand) make_visible() |
|
106 row += 1 |
104 } |
107 } |
105 } |
108 } |
106 tree.setRootVisible(false) |
109 tree.setRootVisible(false) |
107 tree.setVisibleRowCount(visible) |
110 tree.setVisibleRowCount(visible) |
108 } |
111 } |