--- a/src/Pure/PIDE/command.scala Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/command.scala Mon Apr 17 12:20:45 2017 +0200
@@ -451,8 +451,7 @@
val blobs =
files.map(file =>
(Exn.capture {
- val name =
- Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+ val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
(name, blob)
}).user_error)
--- a/src/Pure/PIDE/rendering.scala Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Mon Apr 17 12:20:45 2017 +0200
@@ -423,8 +423,8 @@
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 perhaps_append_file(node_name: Document.Node.Name, name: String): String =
+ if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
{
@@ -451,7 +451,7 @@
Some(info + (r0, true, XML.Text(txt1 + txt2)))
case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
- val file = perhaps_append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name, name)
val text =
if (name == file) "file " + quote(file)
else "path " + quote(name) + "\nfile " + quote(file)
--- a/src/Pure/PIDE/resources.scala Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 17 12:20:45 2017 +0200
@@ -28,6 +28,9 @@
def append(dir: String, source_path: Path): String =
(Path.explode(dir) + source_path).expand.implode
+ def append(node_name: Document.Node.Name, source_path: Path): String =
+ append(node_name.master_dir, source_path)
+
/* source files of Isabelle/ML bootstrap */
--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Apr 17 12:20:45 2017 +0200
@@ -237,7 +237,7 @@
range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
- val file = perhaps_append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name, name)
Some(Line.Node_Range(file) :: links)
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Apr 17 12:20:45 2017 +0200
@@ -195,8 +195,7 @@
if (text == "" || text.endsWith("/")) (path, "")
else (path.dir, path.base.implode)
- val directory =
- new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
+ val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
val files = directory.listFiles
if (files == null) Nil
else {
--- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Apr 17 12:20:45 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 = perhaps_append_file(snapshot.node_name.master_dir, name)
+ val file = perhaps_append_file(snapshot.node_name, name)
val link = JEdit_Editor.hyperlink_file(true, file)
Some(links :+ Text.Info(snapshot.convert(info_range), link))