allow single quote within URL;
authorwenzelm
Wed Jan 27 14:14:06 2016 +0100 (2016-01-27)
changeset 62248dca0bac351b2
parent 62247 ec35b8aca636
child 62249 c1d6dfd645e2
allow single quote within URL;
src/Pure/General/url.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/General/url.scala	Wed Jan 27 14:09:58 2016 +0100
     1.2 +++ b/src/Pure/General/url.scala	Wed Jan 27 14:14:06 2016 +0100
     1.3 @@ -12,6 +12,9 @@
     1.4  
     1.5  object Url
     1.6  {
     1.7 +  def escape(name: String): String =
     1.8 +    (for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString
     1.9 +
    1.10    def apply(name: String): URL =
    1.11    {
    1.12      try { new URL(name) }
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 27 14:09:58 2016 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 27 14:14:06 2016 +0100
     2.3 @@ -223,7 +223,7 @@
     2.4        val external = true
     2.5        def follow(view: View): Unit =
     2.6          Standard_Thread.fork("hyperlink_url") {
     2.7 -          try { Isabelle_System.open(name) }
     2.8 +          try { Isabelle_System.open(Url.escape(name)) }
     2.9            catch {
    2.10              case exn: Throwable =>
    2.11                GUI_Thread.later {