prefer Isabelle/Scala operations;
authorwenzelm
Fri, 25 Apr 2014 20:21:27 +0200
changeset 56729 1da2272a06a4
parent 56728 6dc97c5aaf5e
child 56730 e723f041b6d0
prefer Isabelle/Scala operations;
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/jedit_editor.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 {
--- 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 _ =>
             }
--- 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)
     }