# HG changeset patch
# User wenzelm
# Date 1659437824 -7200
# Node ID 7671f9fc66d74c4c9c9c6e20d918c4a9016a3f68
# Parent  d3430f302c2e64ad874cd9270c5f9891b7d10357
removed somewhat pointless operations (see a6c69599ab99);

diff -r d3430f302c2e -r 7671f9fc66d7 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Jul 30 14:49:22 2022 +0200
+++ b/src/Pure/Thy/export.scala	Tue Aug 02 12:57:04 2022 +0200
@@ -83,17 +83,6 @@
         else None
       }
     }
-
-    def read(dir: Path, cache: XML.Cache): Option[Entry] = {
-      val path = dir + Path.basic(theory) + Path.explode(name)
-      if (path.is_file) {
-        val executable = File.is_executable(path)
-        val uncompressed = Bytes.read(path)
-        val body = Future.value((false, uncompressed))
-        Some(Entry(this, executable, body, cache))
-      }
-      else None
-    }
   }
 
   def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
@@ -323,25 +312,6 @@
 
         override def toString: String = snapshot.toString
       }
-
-    def directory(
-      dir: Path,
-      cache: XML.Cache,
-      session_name: String,
-      theory_name: String
-    ) : Provider = {
-      new Provider {
-        def apply(export_name: String): Option[Entry] =
-          Entry_Name(session = session_name, theory = theory_name, name = export_name)
-            .read(dir, cache)
-
-        def focus(other_theory: String): Provider =
-          if (other_theory == theory_name) this
-          else Provider.directory(dir, cache, session_name, other_theory)
-
-        override def toString: String = dir.toString
-      }
-    }
   }
 
   trait Provider {