--- 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)
}