prefer Isabelle/Scala operations;
authorwenzelm
Fri Apr 25 20:21:27 2014 +0200 (2014-04-25)
changeset 567291da2272a06a4
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
     1.1 --- a/src/Tools/jEdit/src/active.scala	Fri Apr 25 20:07:39 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/active.scala	Fri Apr 25 20:21:27 2014 +0200
     1.3 @@ -30,25 +30,23 @@
     1.4              // FIXME avoid hard-wired stuff
     1.5              elem match {
     1.6                case XML.Elem(Markup(Markup.BROWSER, _), body) =>
     1.7 -                default_thread_pool.submit(() =>
     1.8 -                  {
     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 -                      Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
    1.13 -                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
    1.14 -                  })
    1.15 +                Future.fork {
    1.16 +                  val graph_file = Isabelle_System.tmp_file("graph")
    1.17 +                  File.write(graph_file, XML.content(body))
    1.18 +                  Isabelle_System.bash_env(null,
    1.19 +                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
    1.20 +                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
    1.21 +                }
    1.22  
    1.23                case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
    1.24 -                default_thread_pool.submit(() =>
    1.25 -                  {
    1.26 -                    val graph =
    1.27 -                      Exn.capture {
    1.28 -                        isabelle.graphview.Model.decode_graph(body)
    1.29 -                          .transitive_reduction_acyclic
    1.30 -                      }
    1.31 -                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    1.32 -                  })
    1.33 +                Future.fork {
    1.34 +                  val graph =
    1.35 +                    Exn.capture {
    1.36 +                      isabelle.graphview.Model.decode_graph(body)
    1.37 +                        .transitive_reduction_acyclic
    1.38 +                    }
    1.39 +                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    1.40 +                }
    1.41  
    1.42                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
    1.43                  props match {
     2.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Apr 25 20:07:39 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Fri Apr 25 20:21:27 2014 +0200
     2.3 @@ -68,13 +68,14 @@
     2.4                  if (path.is_file)
     2.5                    PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
     2.6                  else {
     2.7 -                  default_thread_pool.submit(() =>
     2.8 +                  Future.fork {
     2.9                      try { Doc.view(path) }
    2.10                      catch {
    2.11                        case exn: Throwable =>
    2.12                          GUI.error_dialog(view,
    2.13                            "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    2.14 -                    })
    2.15 +                    }
    2.16 +                  }
    2.17                  }
    2.18                case _ =>
    2.19              }
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 20:07:39 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 20:21:27 2014 +0200
     3.3 @@ -162,20 +162,21 @@
     3.4    def hyperlink_url(name: String): Hyperlink =
     3.5      new Hyperlink {
     3.6        val external = true
     3.7 -      def follow(view: View) =
     3.8 -        default_thread_pool.submit(() =>
     3.9 +      def follow(view: View): Unit =
    3.10 +        Future.fork {
    3.11            try { Isabelle_System.open(name) }
    3.12            catch {
    3.13              case exn: Throwable =>
    3.14                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    3.15 -          })
    3.16 +          }
    3.17 +        }
    3.18        override def toString: String = "URL " + quote(name)
    3.19      }
    3.20  
    3.21    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    3.22      new Hyperlink {
    3.23        val external = false
    3.24 -      def follow(view: View) = goto_file(view, name, line, column)
    3.25 +      def follow(view: View): Unit = goto_file(view, name, line, column)
    3.26        override def toString: String = "file " + quote(name)
    3.27      }
    3.28