--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/export.scala Sun May 06 23:03:08 2018 +0200
@@ -0,0 +1,119 @@
+/* Title: Pure/Thy/export.scala
+ Author: Makarius
+
+Manage theory exports.
+*/
+
+package isabelle
+
+object Export
+{
+ /* SQL data model */
+
+ object Data
+ {
+ val session_name = SQL.Column.string("session_name").make_primary_key
+ val theory_name = SQL.Column.string("theory_name").make_primary_key
+ val name = SQL.Column.string("name").make_primary_key
+ val compressed = SQL.Column.bool("compressed")
+ val body = SQL.Column.bytes("body")
+
+ val table =
+ SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
+
+ def where_equal(session_name: String, theory_name: String): SQL.Source =
+ "WHERE " + Data.session_name.equal(session_name) +
+ " AND " + Data.theory_name.equal(theory_name)
+ }
+
+ def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
+ {
+ val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
+ db.using_statement(select)(stmt =>
+ stmt.execute_query().iterator(res => res.string(Data.name)).toList)
+ }
+
+ sealed case class Entry(
+ session_name: String, theory_name: String, name: String, compressed: Boolean, body: Bytes)
+ {
+ override def toString: String = theory_name + ":" + name
+
+ def message(msg: String): String =
+ msg + " " + quote(name) + " for theory " + quote(theory_name)
+
+ lazy val compressed_body: Bytes = if (compressed) body else body.compress()
+ lazy val uncompressed_body: Bytes = if (compressed) body.uncompress() else body
+
+ def write(db: SQL.Database)
+ {
+ db.using_statement(Data.table.insert())(stmt =>
+ {
+ stmt.string(1) = session_name
+ stmt.string(2) = theory_name
+ stmt.string(3) = name
+ stmt.bool(4) = compressed
+ stmt.bytes(5) = body
+ stmt.execute()
+ })
+ }
+ }
+
+ def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
+ {
+ val select =
+ Data.table.select(List(Data.compressed, Data.body),
+ Data.where_equal(session_name, theory_name) + " AND " + Data.name.equal(name))
+ db.using_statement(select)(stmt =>
+ {
+ val res = stmt.execute_query()
+ if (res.next()) {
+ val compressed = res.bool(Data.compressed)
+ val body = res.bytes(Data.body)
+ Entry(session_name, theory_name, name, compressed, body)
+ }
+ else error(Entry(session_name, theory_name, name, false, Bytes.empty).message("Bad export"))
+ })
+ }
+
+
+ /* database consumer thread */
+
+ def consumer(db: SQL.Database): Consumer = new Consumer(db)
+
+ class Consumer private[Export](db: SQL.Database)
+ {
+ db.create_table(Data.table)
+
+ private val export_errors = Synchronized[List[String]](Nil)
+
+ private val consumer =
+ Consumer_Thread.fork(name = "export")(consume = (future: Future[Entry]) =>
+ {
+ val entry = future.join
+
+ db.transaction {
+ if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) {
+ export_errors.change(errs => entry.message("Duplicate export") :: errs)
+ }
+ else entry.write(db)
+ }
+ true
+ })
+
+ def apply(session_name: String, args: Markup.Export.Args, body: Bytes)
+ {
+ consumer.send(
+ if (args.compress)
+ Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress()))
+ else
+ Future.value(Entry(session_name, args.theory_name, args.name, false, body)))
+ }
+
+ def shutdown(close: Boolean = false): List[String] =
+ {
+ consumer.shutdown()
+ if (close) db.close()
+ export_errors.value.reverse
+ }
+ }
+}