allow single quote within URL;
authorwenzelm
Wed, 27 Jan 2016 14:14:06 +0100
changeset 62248 dca0bac351b2
parent 62247 ec35b8aca636
child 62249 c1d6dfd645e2
allow single quote within URL;
src/Pure/General/url.scala
src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Pure/General/url.scala	Wed Jan 27 14:09:58 2016 +0100
+++ b/src/Pure/General/url.scala	Wed Jan 27 14:14:06 2016 +0100
@@ -12,6 +12,9 @@
 
 object Url
 {
+  def escape(name: String): String =
+    (for (c <- name.iterator) yield if (c == '\'') "%27" else new String(Array(c))).mkString
+
   def apply(name: String): URL =
   {
     try { new URL(name) }
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 27 14:09:58 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 27 14:14:06 2016 +0100
@@ -223,7 +223,7 @@
       val external = true
       def follow(view: View): Unit =
         Standard_Thread.fork("hyperlink_url") {
-          try { Isabelle_System.open(name) }
+          try { Isabelle_System.open(Url.escape(name)) }
           catch {
             case exn: Throwable =>
               GUI_Thread.later {