27 { |
27 { |
28 override def toString = |
28 override def toString = |
29 "<html><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>" |
29 "<html><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>" |
30 } |
30 } |
31 |
31 |
32 private case class Text_File(path: Path) |
32 private case class Text_File(name: String, path: Path) |
33 { |
33 { |
34 override def toString = path.base.implode |
34 override def toString = name |
35 } |
35 } |
36 |
36 |
37 private val root = new DefaultMutableTreeNode |
37 private val root = new DefaultMutableTreeNode |
38 docs foreach { |
38 docs foreach { |
39 case Doc.Section(text) => |
39 case Doc.Section(text) => |
40 root.add(new DefaultMutableTreeNode(text)) |
40 root.add(new DefaultMutableTreeNode(text)) |
41 case Doc.Doc(name, title) => |
41 case Doc.Doc(name, title) => |
42 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
42 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
43 .add(new DefaultMutableTreeNode(Documentation(name, title))) |
43 .add(new DefaultMutableTreeNode(Documentation(name, title))) |
44 case Doc.Text_File(path: Path) => |
44 case Doc.Text_File(name: String, path: Path) => |
45 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
45 root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
46 .add(new DefaultMutableTreeNode(Text_File(path.expand))) |
46 .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) |
47 } |
47 } |
48 |
48 |
49 private def documentation_error(exn: Throwable) { |
49 private def documentation_error(exn: Throwable) { |
50 GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn))) |
50 GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn))) |
51 } |
51 } |
63 node.getUserObject match { |
63 node.getUserObject match { |
64 case Documentation(name, _) => |
64 case Documentation(name, _) => |
65 default_thread_pool.submit(() => |
65 default_thread_pool.submit(() => |
66 try { Doc.view(name) } |
66 try { Doc.view(name) } |
67 catch { case exn: Throwable => documentation_error(exn) }) |
67 catch { case exn: Throwable => documentation_error(exn) }) |
68 case Text_File(path) => |
68 case Text_File(_, path) => |
69 try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) } |
69 try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) } |
70 catch { case exn: Throwable => documentation_error(exn) } |
70 catch { case exn: Throwable => documentation_error(exn) } |
71 case _ => |
71 case _ => |
72 } |
72 } |
73 case _ => |
73 case _ => |