tuned signature;
authorwenzelm
Mon Apr 17 12:20:45 2017 +0200 (2017-04-17)
changeset 65488331f09d9535e
parent 65487 7847807b07ce
child 65489 f3076367f4a8
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/rendering.scala
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Apr 17 12:11:02 2017 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Apr 17 12:20:45 2017 +0200
     1.3 @@ -451,8 +451,7 @@
     1.4          val blobs =
     1.5            files.map(file =>
     1.6              (Exn.capture {
     1.7 -              val name =
     1.8 -                Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
     1.9 +              val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
    1.10                val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
    1.11                (name, blob)
    1.12              }).user_error)
     2.1 --- a/src/Pure/PIDE/rendering.scala	Mon Apr 17 12:11:02 2017 +0200
     2.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Apr 17 12:20:45 2017 +0200
     2.3 @@ -423,8 +423,8 @@
     2.4        rev_infos.filter(p => p._1 == important).reverse.map(_._2)
     2.5    }
     2.6  
     2.7 -  def perhaps_append_file(dir: String, name: String): String =
     2.8 -    if (Path.is_valid(name)) session.resources.append(dir, Path.explode(name)) else name
     2.9 +  def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
    2.10 +    if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
    2.11  
    2.12    def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
    2.13    {
    2.14 @@ -451,7 +451,7 @@
    2.15              Some(info + (r0, true, XML.Text(txt1 + txt2)))
    2.16  
    2.17            case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
    2.18 -            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
    2.19 +            val file = perhaps_append_file(snapshot.node_name, name)
    2.20              val text =
    2.21                if (name == file) "file " + quote(file)
    2.22                else "path " + quote(name) + "\nfile " + quote(file)
     3.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 17 12:11:02 2017 +0200
     3.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 12:20:45 2017 +0200
     3.3 @@ -28,6 +28,9 @@
     3.4    def append(dir: String, source_path: Path): String =
     3.5      (Path.explode(dir) + source_path).expand.implode
     3.6  
     3.7 +  def append(node_name: Document.Node.Name, source_path: Path): String =
     3.8 +    append(node_name.master_dir, source_path)
     3.9 +
    3.10  
    3.11    /* source files of Isabelle/ML bootstrap */
    3.12  
     4.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
     4.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 12:20:45 2017 +0200
     4.3 @@ -237,7 +237,7 @@
     4.4        range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
     4.5          {
     4.6            case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
     4.7 -            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
     4.8 +            val file = perhaps_append_file(snapshot.node_name, name)
     4.9              Some(Line.Node_Range(file) :: links)
    4.10  
    4.11            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
     5.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 17 12:11:02 2017 +0200
     5.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 17 12:20:45 2017 +0200
     5.3 @@ -195,8 +195,7 @@
     5.4              if (text == "" || text.endsWith("/")) (path, "")
     5.5              else (path.dir, path.base.implode)
     5.6  
     5.7 -          val directory =
     5.8 -            new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
     5.9 +          val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
    5.10            val files = directory.listFiles
    5.11            if (files == null) Nil
    5.12            else {
     6.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:20:45 2017 +0200
     6.3 @@ -304,7 +304,7 @@
     6.4        range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
     6.5          {
     6.6            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
     6.7 -            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
     6.8 +            val file = perhaps_append_file(snapshot.node_name, name)
     6.9              val link = JEdit_Editor.hyperlink_file(true, file)
    6.10              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    6.11