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