src/Tools/jEdit/src/rendering.scala
changeset 55879 ac979f750c1a
parent 55878 6d092a5166f1
child 55883 6f50d445f0e3
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:37:06 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:58:07 2014 +0100
     1.3 @@ -343,7 +343,7 @@
     1.4        range, Vector.empty, Rendering.hyperlink_elements, _ =>
     1.5          {
     1.6            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
     1.7 -          if Path.is_ok(name) =>
     1.8 +          if Path.is_valid(name) =>
     1.9              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    1.10              val link = PIDE.editor.hyperlink_file(jedit_file)
    1.11              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    1.12 @@ -461,7 +461,7 @@
    1.13                else ""
    1.14              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    1.15            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
    1.16 -          if Path.is_ok(name) =>
    1.17 +          if Path.is_valid(name) =>
    1.18              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    1.19              Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
    1.20            case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>