--- 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)
--- 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) { }
}
-
--- 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), _)))
--- 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), _))) =>