prefer ad-hoc non-worker threads;
authorwenzelm
Tue Nov 03 14:03:44 2015 +0100 (2015-11-03)
changeset 61557f6387515f951
parent 61556 0d4ee4168e41
child 61558 68b86028e02a
prefer ad-hoc non-worker threads;
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Tools/jEdit/src/active.scala	Tue Nov 03 13:54:34 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Nov 03 14:03:44 2015 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4              // FIXME avoid hard-wired stuff
     1.5              elem match {
     1.6                case XML.Elem(Markup(Markup.BROWSER, _), body) =>
     1.7 -                Future.fork {
     1.8 +                Standard_Thread.fork("browser") {
     1.9                    val graph_file = Isabelle_System.tmp_file("graph")
    1.10                    File.write(graph_file, XML.content(body))
    1.11                    Isabelle_System.bash_env(null,
    1.12 @@ -39,7 +39,7 @@
    1.13                  }
    1.14  
    1.15                case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
    1.16 -                Future.fork {
    1.17 +                Standard_Thread.fork("graphview") {
    1.18                    val graph =
    1.19                      Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
    1.20                    GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
     2.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 03 13:54:34 2015 +0100
     2.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Nov 03 14:03:44 2015 +0100
     2.3 @@ -59,7 +59,7 @@
     2.4          if (path.is_file)
     2.5            PIDE.editor.goto_file(true, view, File.platform_path(path))
     2.6          else {
     2.7 -          Future.fork {
     2.8 +          Standard_Thread.fork("documentation") {
     2.9              try { Doc.view(path) }
    2.10              catch {
    2.11                case exn: Throwable =>
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 13:54:34 2015 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 14:03:44 2015 +0100
     3.3 @@ -194,7 +194,7 @@
     3.4      new Hyperlink {
     3.5        val external = true
     3.6        def follow(view: View): Unit =
     3.7 -        Future.fork {
     3.8 +        Standard_Thread.fork("hyperlink_url") {
     3.9            try { Isabelle_System.open(name) }
    3.10            catch {
    3.11              case exn: Throwable =>