clarified signature;
authorwenzelm
Thu May 17 14:40:58 2018 +0200 (4 days ago)
changeset 68202a99180ad3441
parent 68201 dee993b88a7b
child 68203 cda4f24331d5
clarified signature;
src/Pure/Thy/export.scala
     1.1 --- a/src/Pure/Thy/export.scala	Thu May 17 14:01:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Thu May 17 14:40:58 2018 +0200
     1.3 @@ -124,7 +124,8 @@
     1.4        else Future.value((false, body)))
     1.5    }
     1.6  
     1.7 -  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
     1.8 +  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
     1.9 +    : Option[Entry] =
    1.10    {
    1.11      val select =
    1.12        Data.table.select(List(Data.compressed, Data.body),
    1.13 @@ -135,9 +136,9 @@
    1.14        if (res.next()) {
    1.15          val compressed = res.bool(Data.compressed)
    1.16          val body = res.bytes(Data.body)
    1.17 -        Entry(session_name, theory_name, name, Future.value(compressed, body))
    1.18 +        Some(Entry(session_name, theory_name, name, Future.value(compressed, body)))
    1.19        }
    1.20 -      else error(message("Bad export", theory_name, name))
    1.21 +      else None
    1.22      })
    1.23    }
    1.24  
    1.25 @@ -274,11 +275,11 @@
    1.26            val xz_cache = XZ.make_cache()
    1.27  
    1.28            val matcher = make_matcher(export_pattern)
    1.29 -          for { (theory_name, name) <- export_names if matcher(theory_name, name) }
    1.30 -          {
    1.31 -            val entry = read_entry(db, session_name, theory_name, name)
    1.32 +          for {
    1.33 +            (theory_name, name) <- export_names if matcher(theory_name, name)
    1.34 +            entry <- read_entry(db, session_name, theory_name, name)
    1.35 +          } {
    1.36              val path = export_dir + Path.basic(theory_name) + Path.explode(name)
    1.37 -
    1.38              progress.echo("exporting " + path)
    1.39              Isabelle_System.mkdirs(path.dir)
    1.40              Bytes.write(path, entry.uncompressed(cache = xz_cache))