src/Pure/PIDE/resources.scala
changeset 66716 8737b866bd1c
parent 66713 afba7ffd6492
child 66766 19f8385ddfd3
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Sep 29 17:35:09 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 17:41:39 2017 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4  
     1.5    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     1.6    {
     1.7 -    val path = File.check_file(Path.explode(name.node))
     1.8 +    val path = File.check_file(name.path)
     1.9      val reader = Scan.byte_reader(path.file)
    1.10      try { f(reader) } finally { reader.close }
    1.11    }