# HG changeset patch # User wenzelm # Date 1373141815 -7200 # Node ID 6f5678b97c4ecef3d78fd9987bda4b953a611983 # Parent 19d674acb7649eed272ac55fd261d48e1579b6a7 eliminated pointless catch of unlikely exceptions, which may occur in Doc.contents already; diff -r 19d674acb764 -r 6f5678b97c4e src/Tools/jEdit/src/documentation_dockable.scala --- 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 _ =>