|
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, GridLayout} |
|
13 import javax.swing.{JTree, JScrollPane} |
|
14 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel} |
|
15 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} |
|
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 Swing_Thread.require() |
|
23 |
|
24 private val docs = Doc.contents() |
|
25 |
|
26 private case class Documentation(name: String, title: String) |
|
27 { |
|
28 override def toString = |
|
29 "<html><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>" |
|
30 } |
|
31 |
|
32 private val root = new DefaultMutableTreeNode |
|
33 docs foreach { |
|
34 case Doc.Section(text) => |
|
35 root.add(new DefaultMutableTreeNode(text)) |
|
36 case Doc.Doc(name, title) => |
|
37 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
|
38 .add(new DefaultMutableTreeNode(Documentation(name, title))) |
|
39 } |
|
40 |
|
41 private val tree = new JTree(root) |
|
42 if (!OperatingSystem.isMacOSLF) |
|
43 tree.putClientProperty("JTree.lineStyle", "Angled") |
|
44 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
|
45 tree.addTreeSelectionListener( |
|
46 new TreeSelectionListener { |
|
47 override def valueChanged(e: TreeSelectionEvent) |
|
48 { |
|
49 tree.getLastSelectedPathComponent match { |
|
50 case node: DefaultMutableTreeNode => |
|
51 node.getUserObject match { |
|
52 case Documentation(name, _) => Doc.view(name) |
|
53 case _ => |
|
54 } |
|
55 case _ => |
|
56 } |
|
57 } |
|
58 }) |
|
59 tree.setRootVisible(false) |
|
60 tree.setVisibleRowCount(docs.length) |
|
61 (0 until docs.length).foreach(tree.expandRow) |
|
62 |
|
63 private val tree_view = new JScrollPane(tree) |
|
64 tree_view.setMinimumSize(new Dimension(100, 50)) |
|
65 |
|
66 set_content(tree_view) |
|
67 } |