src/Pure/PIDE/resources.scala
changeset 64654 31b681e38c70
parent 63584 68751fe1c036
child 64656 65c8a7780538
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Dec 21 23:30:13 2016 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Dec 21 23:54:21 2016 +0100
     1.3 @@ -43,6 +43,15 @@
     1.4    def append(dir: String, source_path: Path): String =
     1.5      (Path.explode(dir) + source_path).expand.implode
     1.6  
     1.7 +  def append_file(dir: String, raw_name: String): String =
     1.8 +    if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
     1.9 +    else raw_name
    1.10 +
    1.11 +  def append_file_url(dir: String, raw_name: String): String =
    1.12 +    if (Path.is_valid(raw_name)) "file://" + append(dir, Path.explode(raw_name))
    1.13 +    else raw_name
    1.14 +
    1.15 +
    1.16    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.17    {
    1.18      val path = Path.explode(name.node)
    1.19 @@ -133,4 +142,3 @@
    1.20  
    1.21    def commit(change: Session.Change) { }
    1.22  }
    1.23 -