src/Tools/jEdit/src/jedit_editor.scala
changeset 62248 dca0bac351b2
parent 62062 ee610059b0e9
child 64521 1aef5a0e18d7
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 27 14:09:58 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 27 14:14:06 2016 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4        val external = true
     1.5        def follow(view: View): Unit =
     1.6          Standard_Thread.fork("hyperlink_url") {
     1.7 -          try { Isabelle_System.open(name) }
     1.8 +          try { Isabelle_System.open(Url.escape(name)) }
     1.9            catch {
    1.10              case exn: Throwable =>
    1.11                GUI_Thread.later {