eliminated pointless catch of unlikely exceptions, which may occur in Doc.contents already;
--- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Jul 06 22:11:18 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Jul 06 22:16:55 2013 +0200
@@ -46,10 +46,6 @@
.add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
}
- private def documentation_error(exn: Throwable) {
- GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn)))
- }
-
private val tree = new JTree(root)
if (!OperatingSystem.isMacOSLF)
tree.putClientProperty("JTree.lineStyle", "Angled")
@@ -64,10 +60,13 @@
case Documentation(name, _) =>
default_thread_pool.submit(() =>
try { Doc.view(name) }
- catch { case exn: Throwable => documentation_error(exn) })
+ catch {
+ case exn: Throwable =>
+ GUI.error_dialog(view,
+ "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+ })
case Text_File(_, path) =>
- try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
- catch { case exn: Throwable => documentation_error(exn) }
+ Hyperlink(Isabelle_System.platform_path(path)).follow(view)
case _ =>
}
case _ =>