# HG changeset patch
# User wenzelm
# Date 1453900446 -3600
# Node ID dca0bac351b2e423a9b492840e6a22d397d0dd17
# Parent  ec35b8aca63694539bcfb3d42a6cf580f151c7c2
allow single quote within URL;

diff -r ec35b8aca636 -r dca0bac351b2 src/Pure/General/url.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) }
diff -r ec35b8aca636 -r dca0bac351b2 src/Tools/jEdit/src/jedit_editor.scala
--- 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 {