# HG changeset patch
# User wenzelm
# Date 1482402059 -3600
# Node ID 65c8a7780538674e0f62e825aafad8591ca31e15
# Parent  ea34f36ff6a5af9190bd3bd37677de9afbd9b520
tuned;

diff -r ea34f36ff6a5 -r 65c8a7780538 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 22 11:08:58 2016 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 22 11:20:59 2016 +0100
@@ -52,15 +52,6 @@
     else raw_name
 
 
-  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
-  {
-    val path = Path.explode(name.node)
-    if (!path.is_file) error("No such file: " + path.toString)
-
-    val reader = Scan.byte_reader(path.file)
-    try { f(reader) } finally { reader.close }
-  }
-
 
   /* theory files */
 
@@ -96,6 +87,15 @@
     }
   }
 
+  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
+  {
+    val path = Path.explode(name.node)
+    if (!path.is_file) error("No such file: " + path.toString)
+
+    val reader = Scan.byte_reader(path.file)
+    try { f(reader) } finally { reader.close }
+  }
+
   def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
     reader: Reader[Char], start: Token.Pos): Document.Node.Header =
   {