equal
deleted
inserted
replaced
44 case Doc.Text_File(name: String, 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(name, path.expand))) |
46 .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) |
47 } |
47 } |
48 |
48 |
49 private def documentation_error(exn: Throwable) { |
|
50 GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn))) |
|
51 } |
|
52 |
|
53 private val tree = new JTree(root) |
49 private val tree = new JTree(root) |
54 if (!OperatingSystem.isMacOSLF) |
50 if (!OperatingSystem.isMacOSLF) |
55 tree.putClientProperty("JTree.lineStyle", "Angled") |
51 tree.putClientProperty("JTree.lineStyle", "Angled") |
56 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
52 tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) |
57 tree.addTreeSelectionListener( |
53 tree.addTreeSelectionListener( |
62 case node: DefaultMutableTreeNode => |
58 case node: DefaultMutableTreeNode => |
63 node.getUserObject match { |
59 node.getUserObject match { |
64 case Documentation(name, _) => |
60 case Documentation(name, _) => |
65 default_thread_pool.submit(() => |
61 default_thread_pool.submit(() => |
66 try { Doc.view(name) } |
62 try { Doc.view(name) } |
67 catch { case exn: Throwable => documentation_error(exn) }) |
63 catch { |
|
64 case exn: Throwable => |
|
65 GUI.error_dialog(view, |
|
66 "Documentation error", GUI.scrollable_text(Exn.message(exn))) |
|
67 }) |
68 case Text_File(_, path) => |
68 case Text_File(_, path) => |
69 try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) } |
69 Hyperlink(Isabelle_System.platform_path(path)).follow(view) |
70 catch { case exn: Throwable => documentation_error(exn) } |
|
71 case _ => |
70 case _ => |
72 } |
71 } |
73 case _ => |
72 case _ => |
74 } |
73 } |
75 } |
74 } |