# HG changeset patch
# User wenzelm
# Date 1398450087 -7200
# Node ID 1da2272a06a451a3cb20414056cc6e921703ea0a
# Parent  6dc97c5aaf5e8a021e7fa84469253518fde0e843
prefer Isabelle/Scala operations;

diff -r 6dc97c5aaf5e -r 1da2272a06a4 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Apr 25 20:07:39 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Apr 25 20:21:27 2014 +0200
@@ -30,25 +30,23 @@
             // FIXME avoid hard-wired stuff
             elem match {
               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
-                default_thread_pool.submit(() =>
-                  {
-                    val graph_file = Isabelle_System.tmp_file("graph")
-                    File.write(graph_file, XML.content(body))
-                    Isabelle_System.bash_env(null,
-                      Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
-                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
-                  })
+                Future.fork {
+                  val graph_file = Isabelle_System.tmp_file("graph")
+                  File.write(graph_file, XML.content(body))
+                  Isabelle_System.bash_env(null,
+                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
+                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
+                }
 
               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
-                default_thread_pool.submit(() =>
-                  {
-                    val graph =
-                      Exn.capture {
-                        isabelle.graphview.Model.decode_graph(body)
-                          .transitive_reduction_acyclic
-                      }
-                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
-                  })
+                Future.fork {
+                  val graph =
+                    Exn.capture {
+                      isabelle.graphview.Model.decode_graph(body)
+                        .transitive_reduction_acyclic
+                    }
+                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
+                }
 
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                 props match {
diff -r 6dc97c5aaf5e -r 1da2272a06a4 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Apr 25 20:07:39 2014 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Apr 25 20:21:27 2014 +0200
@@ -68,13 +68,14 @@
                 if (path.is_file)
                   PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
                 else {
-                  default_thread_pool.submit(() =>
+                  Future.fork {
                     try { Doc.view(path) }
                     catch {
                       case exn: Throwable =>
                         GUI.error_dialog(view,
                           "Documentation error", GUI.scrollable_text(Exn.message(exn)))
-                    })
+                    }
+                  }
                 }
               case _ =>
             }
diff -r 6dc97c5aaf5e -r 1da2272a06a4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 20:07:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 20:21:27 2014 +0200
@@ -162,20 +162,21 @@
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
       val external = true
-      def follow(view: View) =
-        default_thread_pool.submit(() =>
+      def follow(view: View): Unit =
+        Future.fork {
           try { Isabelle_System.open(name) }
           catch {
             case exn: Throwable =>
               GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
-          })
+          }
+        }
       override def toString: String = "URL " + quote(name)
     }
 
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink {
       val external = false
-      def follow(view: View) = goto_file(view, name, line, column)
+      def follow(view: View): Unit = goto_file(view, name, line, column)
       override def toString: String = "file " + quote(name)
     }