clarified signature;
authorwenzelm
Wed Dec 21 23:54:21 2016 +0100 (2016-12-21)
changeset 6465431b681e38c70
parent 64653 89c5bb2a2128
child 64655 ea34f36ff6a5
clarified signature;
src/Pure/PIDE/rendering.scala
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Wed Dec 21 23:30:13 2016 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Dec 21 23:54:21 2016 +0100
     1.3 @@ -39,19 +39,6 @@
     1.4    override def toString: String = "Rendering(" + snapshot.toString + ")"
     1.5  
     1.6  
     1.7 -  /* resources */
     1.8 -
     1.9 -  def resolve_file(name: String): String =
    1.10 -    if (Path.is_valid(name))
    1.11 -      resources.append(snapshot.node_name.master_dir, Path.explode(name))
    1.12 -    else name
    1.13 -
    1.14 -  def resolve_file_url(name: String): String =
    1.15 -    if (Path.is_valid(name))
    1.16 -      "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name))
    1.17 -    else name
    1.18 -
    1.19 -
    1.20    /* tooltips */
    1.21  
    1.22    def tooltip_margin: Int
    1.23 @@ -94,7 +81,7 @@
    1.24              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    1.25  
    1.26            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
    1.27 -            val file = resolve_file(name)
    1.28 +            val file = resources.append_file(snapshot.node_name.master_dir, name)
    1.29              val text =
    1.30                if (name == file) "file " + quote(file)
    1.31                else "path " + quote(name) + "\nfile " + quote(file)
     2.1 --- a/src/Pure/PIDE/resources.scala	Wed Dec 21 23:30:13 2016 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Wed Dec 21 23:54:21 2016 +0100
     2.3 @@ -43,6 +43,15 @@
     2.4    def append(dir: String, source_path: Path): String =
     2.5      (Path.explode(dir) + source_path).expand.implode
     2.6  
     2.7 +  def append_file(dir: String, raw_name: String): String =
     2.8 +    if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
     2.9 +    else raw_name
    2.10 +
    2.11 +  def append_file_url(dir: String, raw_name: String): String =
    2.12 +    if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name))
    2.13 +    else raw_name
    2.14 +
    2.15 +
    2.16    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    2.17    {
    2.18      val path = Path.explode(name.node)
    2.19 @@ -133,4 +142,3 @@
    2.20  
    2.21    def commit(change: Session.Change) { }
    2.22  }
    2.23 -
     3.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 23:30:13 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 23:54:21 2016 +0100
     3.3 @@ -37,7 +37,8 @@
     3.4        range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
     3.5          {
     3.6            case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
     3.7 -            Some(Line.Node_Range(resolve_file_url(name)) :: links)
     3.8 +            val file = resources.append_file_url(snapshot.node_name.master_dir, name)
     3.9 +            Some(Line.Node_Range(file) :: links)
    3.10  
    3.11  /* FIXME
    3.12            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
     4.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 21 23:30:13 2016 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 21 23:54:21 2016 +0100
     4.3 @@ -466,7 +466,8 @@
     4.4        range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
     4.5          {
     4.6            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
     4.7 -            val link = PIDE.editor.hyperlink_file(true, resolve_file(name))
     4.8 +            val file = resources.append_file(snapshot.node_name.master_dir, name)
     4.9 +            val link = PIDE.editor.hyperlink_file(true, file)
    4.10              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    4.11  
    4.12            case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>