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