src/Tools/jEdit/src/jedit_editor.scala
changeset 56729 1da2272a06a4
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 20:07:39 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 20:21:27 2014 +0200
     1.3 @@ -162,20 +162,21 @@
     1.4    def hyperlink_url(name: String): Hyperlink =
     1.5      new Hyperlink {
     1.6        val external = true
     1.7 -      def follow(view: View) =
     1.8 -        default_thread_pool.submit(() =>
     1.9 +      def follow(view: View): Unit =
    1.10 +        Future.fork {
    1.11            try { Isabelle_System.open(name) }
    1.12            catch {
    1.13              case exn: Throwable =>
    1.14                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
    1.15 -          })
    1.16 +          }
    1.17 +        }
    1.18        override def toString: String = "URL " + quote(name)
    1.19      }
    1.20  
    1.21    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.22      new Hyperlink {
    1.23        val external = false
    1.24 -      def follow(view: View) = goto_file(view, name, line, column)
    1.25 +      def follow(view: View): Unit = goto_file(view, name, line, column)
    1.26        override def toString: String = "file " + quote(name)
    1.27      }
    1.28