# HG changeset patch # User wenzelm # Date 1535452777 -7200 # Node ID a6c69599ab99906f16413cb4492366246e90ebf5 # Parent 44ec6fdaacf8b8eb1b44a5b1da58c48083a09ba0 Export.Provider for "isabelle dump" output_dir; diff -r 44ec6fdaacf8 -r a6c69599ab99 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Tue Aug 28 12:07:30 2018 +0200 +++ b/src/Pure/Thy/export.scala Tue Aug 28 12:39:37 2018 +0200 @@ -150,6 +150,16 @@ }) } + def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] = + { + val path = dir + Path.basic(theory_name) + Path.explode(name) + if (path.is_file) { + val uncompressed = Bytes.read(path) + Some(Entry(session_name, theory_name, name, Future.value((false, uncompressed)))) + } + else None + } + /* database consumer thread */ @@ -200,6 +210,12 @@ def apply(export_name: String): Option[Entry] = snapshot.exports_map.get(export_name) } + + def directory(dir: Path, session_name: String, theory_name: String): Provider = + new Provider { + def apply(export_name: String): Option[Entry] = + read_entry(dir, session_name, theory_name, export_name) + } } trait Provider