# HG changeset patch
# User wenzelm
# Date 1492423862 -7200
# Node ID 7847807b07ce0359c662c39b3e85a8dd45c289a2
# Parent  8c7bc3a13513d5a96e2de799f3e4a1e90ffa6480
tuned signature;

diff -r 8c7bc3a13513 -r 7847807b07ce src/Pure/PIDE/rendering.scala
--- 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)
diff -r 8c7bc3a13513 -r 7847807b07ce src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 12:11:02 2017 +0200
@@ -28,11 +28,6 @@
   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
-
-
 
   /* source files of Isabelle/ML bootstrap */
 
diff -r 8c7bc3a13513 -r 7847807b07ce src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
@@ -237,7 +237,7 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            val file = model.resources.append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
             Some(Line.Node_Range(file) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
diff -r 8c7bc3a13513 -r 7847807b07ce src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
@@ -304,7 +304,7 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val file = PIDE.resources.append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
             val link = JEdit_Editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))