# HG changeset patch
# User wenzelm
# Date 1446555824 -3600
# Node ID f6387515f9510b4bed3b33002ce2f740f3538e0c
# Parent  0d4ee4168e41694baabbe92dfe46e86298c6cbaa
prefer ad-hoc non-worker threads;

diff -r 0d4ee4168e41 -r f6387515f951 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Tue Nov 03 13:54:34 2015 +0100
+++ b/src/Tools/jEdit/src/active.scala	Tue Nov 03 14:03:44 2015 +0100
@@ -30,7 +30,7 @@
             // FIXME avoid hard-wired stuff
             elem match {
               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
-                Future.fork {
+                Standard_Thread.fork("browser") {
                   val graph_file = Isabelle_System.tmp_file("graph")
                   File.write(graph_file, XML.content(body))
                   Isabelle_System.bash_env(null,
@@ -39,7 +39,7 @@
                 }
 
               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
-                Future.fork {
+                Standard_Thread.fork("graphview") {
                   val graph =
                     Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
                   GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
diff -r 0d4ee4168e41 -r f6387515f951 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 03 13:54:34 2015 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 03 14:03:44 2015 +0100
@@ -59,7 +59,7 @@
         if (path.is_file)
           PIDE.editor.goto_file(true, view, File.platform_path(path))
         else {
-          Future.fork {
+          Standard_Thread.fork("documentation") {
             try { Doc.view(path) }
             catch {
               case exn: Throwable =>
diff -r 0d4ee4168e41 -r f6387515f951 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 13:54:34 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 14:03:44 2015 +0100
@@ -194,7 +194,7 @@
     new Hyperlink {
       val external = true
       def follow(view: View): Unit =
-        Future.fork {
+        Standard_Thread.fork("hyperlink_url") {
           try { Isabelle_System.open(name) }
           catch {
             case exn: Throwable =>