10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import java.awt.Dimension |
12 import java.awt.Dimension |
13 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter} |
13 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter} |
14 import javax.swing.JScrollPane |
14 import javax.swing.JScrollPane |
15 import javax.swing.tree.DefaultMutableTreeNode |
|
16 |
15 |
17 import org.gjt.sp.jedit.{View, OperatingSystem} |
16 import org.gjt.sp.jedit.{View, OperatingSystem} |
18 |
17 |
19 |
18 |
20 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) { |
19 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) { |
25 } |
24 } |
26 |
25 |
27 private val tree = new Tree_View(single_selection_mode = true) |
26 private val tree = new Tree_View(single_selection_mode = true) |
28 |
27 |
29 for (section <- doc_contents.sections) { |
28 for (section <- doc_contents.sections) { |
30 tree.root.add(new DefaultMutableTreeNode(section.title)) |
29 tree.root.add(Tree_View.Node(section.title)) |
31 section.entries.foreach( |
30 section.entries.foreach( |
32 { |
31 { |
33 case entry @ Doc.Doc(name, title, _) => |
32 case entry @ Doc.Doc(name, title, _) => |
34 val string = "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" |
33 val string = "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" |
35 tree.root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
34 tree.root.getLastChild.asInstanceOf[Tree_View.Node] |
36 .add(new DefaultMutableTreeNode(Node(string, entry))) |
35 .add(Tree_View.Node(Node(string, entry))) |
37 case entry @ Doc.Text_File(name: String, _) => |
36 case entry @ Doc.Text_File(name: String, _) => |
38 tree.root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
37 tree.root.getLastChild.asInstanceOf[Tree_View.Node] |
39 .add(new DefaultMutableTreeNode(Node(name, entry))) |
38 .add(Tree_View.Node(Node(name, entry))) |
40 }) |
39 }) |
41 } |
40 } |
42 |
41 |
43 override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow |
42 override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow |
44 |
43 |
45 private def action(node: DefaultMutableTreeNode): Unit = { |
44 private def action(node: Tree_View.Node): Unit = { |
46 node.getUserObject match { |
45 node.getUserObject match { |
47 case Node(_, Doc.Doc(_, _, path)) => |
46 case Node(_, Doc.Doc(_, _, path)) => |
48 PIDE.editor.goto_doc(view, path) |
47 PIDE.editor.goto_doc(view, path) |
49 case Node(_, Doc.Text_File(_, path)) => |
48 case Node(_, Doc.Text_File(_, path)) => |
50 PIDE.editor.goto_file(true, view, File.platform_path(path)) |
49 PIDE.editor.goto_file(true, view, File.platform_path(path)) |
69 tree.addMouseListener(new MouseAdapter { |
68 tree.addMouseListener(new MouseAdapter { |
70 override def mouseClicked(e: MouseEvent): Unit = { |
69 override def mouseClicked(e: MouseEvent): Unit = { |
71 val click = tree.getPathForLocation(e.getX, e.getY) |
70 val click = tree.getPathForLocation(e.getX, e.getY) |
72 if (click != null && e.getClickCount == 1) { |
71 if (click != null && e.getClickCount == 1) { |
73 (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { |
72 (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { |
74 case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 => |
73 case (node: Tree_View.Node, node1: Tree_View.Node) if node == node1 => action(node) |
75 action(node) |
|
76 case _ => |
74 case _ => |
77 } |
75 } |
78 } |
76 } |
79 } |
77 } |
80 }) |
78 }) |