--- a/src/Pure/PIDE/rendering.scala Mon Apr 17 07:44:21 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Mon Apr 17 12:11:02 2017 +0200
@@ -423,6 +423,9 @@
rev_infos.filter(p => p._1 == important).reverse.map(_._2)
}
+ def perhaps_append_file(dir: String, name: String): String =
+ if (Path.is_valid(name)) session.resources.append(dir, Path.explode(name)) else name
+
def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
{
val results =
@@ -448,7 +451,7 @@
Some(info + (r0, true, XML.Text(txt1 + txt2)))
case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
- val file = session.resources.append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name.master_dir, name)
val text =
if (name == file) "file " + quote(file)
else "path " + quote(name) + "\nfile " + quote(file)