# HG changeset patch
# User wenzelm
# Date 1482360861 -3600
# Node ID 31b681e38c703ef722024a39d938edcc47bc8cb7
# Parent  89c5bb2a21280f773b8f7ac1e8e114252c4bbac1
clarified signature;

diff -r 89c5bb2a2128 -r 31b681e38c70 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Dec 21 23:30:13 2016 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 21 23:54:21 2016 +0100
@@ -39,19 +39,6 @@
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
 
-  /* resources */
-
-  def resolve_file(name: String): String =
-    if (Path.is_valid(name))
-      resources.append(snapshot.node_name.master_dir, Path.explode(name))
-    else name
-
-  def resolve_file_url(name: String): String =
-    if (Path.is_valid(name))
-      "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name))
-    else name
-
-
   /* tooltips */
 
   def tooltip_margin: Int
@@ -94,7 +81,7 @@
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
 
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
-            val file = resolve_file(name)
+            val file = resources.append_file(snapshot.node_name.master_dir, name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
diff -r 89c5bb2a2128 -r 31b681e38c70 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Dec 21 23:30:13 2016 +0100
+++ b/src/Pure/PIDE/resources.scala	Wed Dec 21 23:54:21 2016 +0100
@@ -43,6 +43,15 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
+  def append_file(dir: String, raw_name: String): String =
+    if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
+    else raw_name
+
+  def append_file_url(dir: String, raw_name: String): String =
+    if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name))
+    else raw_name
+
+
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = Path.explode(name.node)
@@ -133,4 +142,3 @@
 
   def commit(change: Session.Change) { }
 }
-
diff -r 89c5bb2a2128 -r 31b681e38c70 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 23:30:13 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 23:54:21 2016 +0100
@@ -37,7 +37,8 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            Some(Line.Node_Range(resolve_file_url(name)) :: links)
+            val file = resources.append_file_url(snapshot.node_name.master_dir, name)
+            Some(Line.Node_Range(file) :: links)
 
 /* FIXME
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
diff -r 89c5bb2a2128 -r 31b681e38c70 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 21 23:30:13 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 21 23:54:21 2016 +0100
@@ -466,7 +466,8 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val link = PIDE.editor.hyperlink_file(true, resolve_file(name))
+            val file = resources.append_file(snapshot.node_name.master_dir, name)
+            val link = PIDE.editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>