--- 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 {