--- a/src/Tools/jEdit/src/rendering.scala Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Mar 03 11:58:07 2014 +0100
@@ -343,7 +343,7 @@
range, Vector.empty, Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
- if Path.is_ok(name) =>
+ if Path.is_valid(name) =>
val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
val link = PIDE.editor.hyperlink_file(jedit_file)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
@@ -461,7 +461,7 @@
else ""
Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
- if Path.is_ok(name) =>
+ if Path.is_valid(name) =>
val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>