src/Tools/jEdit/src/jedit_editor.scala
changeset 54702 3daeba5130f0
parent 54531 8330faaeebd5
child 54706 d3c656f0b7ab
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 09:44:57 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 09 12:16:52 2013 +0100
     1.3 @@ -135,6 +135,17 @@
     1.4      }
     1.5    }
     1.6  
     1.7 +  override def hyperlink_url(name: String): Hyperlink =
     1.8 +    new Hyperlink {
     1.9 +      def follow(view: View) =
    1.10 +        default_thread_pool.submit(() =>
    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 hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.19      new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
    1.20