src/Pure/Thy/export.scala
changeset 68831 a6c69599ab99
parent 68418 366e43cddd20
child 68832 9b9fc9ea9dd1
     1.1 --- a/src/Pure/Thy/export.scala	Tue Aug 28 12:07:30 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Tue Aug 28 12:39:37 2018 +0200
     1.3 @@ -150,6 +150,16 @@
     1.4      })
     1.5    }
     1.6  
     1.7 +  def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] =
     1.8 +  {
     1.9 +    val path = dir + Path.basic(theory_name) + Path.explode(name)
    1.10 +    if (path.is_file) {
    1.11 +      val uncompressed = Bytes.read(path)
    1.12 +      Some(Entry(session_name, theory_name, name, Future.value((false, uncompressed))))
    1.13 +    }
    1.14 +    else None
    1.15 +  }
    1.16 +
    1.17  
    1.18    /* database consumer thread */
    1.19  
    1.20 @@ -200,6 +210,12 @@
    1.21          def apply(export_name: String): Option[Entry] =
    1.22            snapshot.exports_map.get(export_name)
    1.23        }
    1.24 +
    1.25 +    def directory(dir: Path, session_name: String, theory_name: String): Provider =
    1.26 +      new Provider {
    1.27 +        def apply(export_name: String): Option[Entry] =
    1.28 +          read_entry(dir, session_name, theory_name, export_name)
    1.29 +      }
    1.30    }
    1.31  
    1.32    trait Provider