eliminated pointless catch of unlikely exceptions, which may occur in Doc.contents already;
authorwenzelm
Sat, 06 Jul 2013 22:16:55 +0200
changeset 52543 6f5678b97c4e
parent 52542 19d674acb764
child 52544 0c4b140cff00
eliminated pointless catch of unlikely exceptions, which may occur in Doc.contents already;
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 _ =>