# HG changeset patch
# User wenzelm
# Date 1552338794 -3600
# Node ID 20b32ade002469e7e7cd0687ff5a5a38d23ad48d
# Parent  18a61caf5e68f4f4a724a462b3e614789fd3f393
clarified signature;

diff -r 18a61caf5e68 -r 20b32ade0024 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Mon Mar 11 20:47:04 2019 +0100
+++ b/src/Pure/General/url.scala	Mon Mar 11 22:13:14 2019 +0100
@@ -10,13 +10,25 @@
 import java.io.{File => JFile}
 import java.nio.file.{Paths, FileSystemNotFoundException}
 import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
+import java.util.Locale
 import java.util.zip.GZIPInputStream
 
 
 object Url
 {
-  def escape(name: String): String =
-    (for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString
+  /* special characters */
+
+  def escape_special(c: Char): String =
+    if ("!#$&'()*+,/:;=?@[]".contains(c)) String.format(Locale.ROOT, "%%%02X", new Integer(c.toInt))
+    else c.toString
+
+  def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString
+
+  def escape_name(name: String): String =
+    name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString
+
+
+  /* make and check URLs */
 
   def apply(name: String): URL =
   {
diff -r 18a61caf5e68 -r 20b32ade0024 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 11 20:47:04 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 11 22:13:14 2019 +0100
@@ -203,7 +203,7 @@
       override val external = true
       def follow(view: View): Unit =
         Standard_Thread.fork("hyperlink_url") {
-          try { Isabelle_System.open(Url.escape(name)) }
+          try { Isabelle_System.open(Url.escape_name(name)) }
           catch {
             case exn: Throwable =>
               GUI_Thread.later {