clarified signature;
authorwenzelm
Mon Mar 11 22:13:14 2019 +0100 (6 weeks ago ago)
changeset 7008220b32ade0024
parent 70081 18a61caf5e68
child 70083 9c697c7ad8d6
clarified signature;
src/Pure/General/url.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/General/url.scala	Mon Mar 11 20:47:04 2019 +0100
     1.2 +++ b/src/Pure/General/url.scala	Mon Mar 11 22:13:14 2019 +0100
     1.3 @@ -10,13 +10,25 @@
     1.4  import java.io.{File => JFile}
     1.5  import java.nio.file.{Paths, FileSystemNotFoundException}
     1.6  import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
     1.7 +import java.util.Locale
     1.8  import java.util.zip.GZIPInputStream
     1.9  
    1.10  
    1.11  object Url
    1.12  {
    1.13 -  def escape(name: String): String =
    1.14 -    (for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString
    1.15 +  /* special characters */
    1.16 +
    1.17 +  def escape_special(c: Char): String =
    1.18 +    if ("!#$&'()*+,/:;=?@[]".contains(c)) String.format(Locale.ROOT, "%%%02X", new Integer(c.toInt))
    1.19 +    else c.toString
    1.20 +
    1.21 +  def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString
    1.22 +
    1.23 +  def escape_name(name: String): String =
    1.24 +    name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString
    1.25 +
    1.26 +
    1.27 +  /* make and check URLs */
    1.28  
    1.29    def apply(name: String): URL =
    1.30    {
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 11 20:47:04 2019 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 11 22:13:14 2019 +0100
     2.3 @@ -203,7 +203,7 @@
     2.4        override val external = true
     2.5        def follow(view: View): Unit =
     2.6          Standard_Thread.fork("hyperlink_url") {
     2.7 -          try { Isabelle_System.open(Url.escape(name)) }
     2.8 +          try { Isabelle_System.open(Url.escape_name(name)) }
     2.9            catch {
    2.10              case exn: Throwable =>
    2.11                GUI_Thread.later {