tuned;
authorwenzelm
Thu Dec 22 11:20:59 2016 +0100 (2016-12-22)
changeset 6465665c8a7780538
parent 64655 ea34f36ff6a5
child 64657 6209e0f7a4e8
tuned;
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Thu Dec 22 11:08:58 2016 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Thu Dec 22 11:20:59 2016 +0100
     1.3 @@ -52,15 +52,6 @@
     1.4      else raw_name
     1.5  
     1.6  
     1.7 -  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     1.8 -  {
     1.9 -    val path = Path.explode(name.node)
    1.10 -    if (!path.is_file) error("No such file: " + path.toString)
    1.11 -
    1.12 -    val reader = Scan.byte_reader(path.file)
    1.13 -    try { f(reader) } finally { reader.close }
    1.14 -  }
    1.15 -
    1.16  
    1.17    /* theory files */
    1.18  
    1.19 @@ -96,6 +87,15 @@
    1.20      }
    1.21    }
    1.22  
    1.23 +  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.24 +  {
    1.25 +    val path = Path.explode(name.node)
    1.26 +    if (!path.is_file) error("No such file: " + path.toString)
    1.27 +
    1.28 +    val reader = Scan.byte_reader(path.file)
    1.29 +    try { f(reader) } finally { reader.close }
    1.30 +  }
    1.31 +
    1.32    def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
    1.33      reader: Reader[Char], start: Token.Pos): Document.Node.Header =
    1.34    {