# HG changeset patch
# User wenzelm
# Date 1372180417 -7200
# Node ID 9a74000426e2f4a069794c736be88221f6649df5
# Parent  c4a70058ff20ffb1199b99062a94ad1f0290e2ad
more robust Doc.view invocation: avoid executing process on GUI thread, but show errors as dialog;

diff -r c4a70058ff20 -r 9a74000426e2 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Jun 25 17:14:50 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Jun 25 19:13:37 2013 +0200
@@ -49,7 +49,14 @@
         tree.getLastSelectedPathComponent match {
           case node: DefaultMutableTreeNode =>
             node.getUserObject match {
-              case Documentation(name, _) => Doc.view(name)
+              case Documentation(name, _) =>
+                default_thread_pool.submit(() =>
+                  try { Doc.view(name) }
+                  catch {
+                    case exn: Throwable =>
+                      GUI.error_dialog(view,
+                        "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+                  })
               case _ =>
             }
           case _ =>