src/Pure/Thy/export.scala
author wenzelm
Wed, 25 Nov 2020 13:06:03 +0100
changeset 72702 79a19657c170
parent 72691 2126cf946086
child 72730 01c9b3033036
permissions -rw-r--r--
clarified names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/export.scala
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     3
68102
813b5d0904c6 clarified signature;
wenzelm
parents: 68101
diff changeset
     4
Manage theory exports: compressed blobs.
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     5
*/
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     6
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     7
package isabelle
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
     8
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
     9
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    10
import scala.annotation.tailrec
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    11
import scala.util.matching.Regex
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    12
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    13
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    14
object Export
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    15
{
72691
2126cf946086 clarified signature;
wenzelm
parents: 72683
diff changeset
    16
  /* artefact names */
2126cf946086 clarified signature;
wenzelm
parents: 72683
diff changeset
    17
72702
79a19657c170 clarified names;
wenzelm
parents: 72691
diff changeset
    18
  val MARKUP = "PIDE/markup"
79a19657c170 clarified names;
wenzelm
parents: 72691
diff changeset
    19
  val MESSAGES = "PIDE/messages"
72691
2126cf946086 clarified signature;
wenzelm
parents: 72683
diff changeset
    20
  val DOCUMENT_PREFIX = "document/"
2126cf946086 clarified signature;
wenzelm
parents: 72683
diff changeset
    21
  val THEORY_PREFIX: String = "theory/"
2126cf946086 clarified signature;
wenzelm
parents: 72683
diff changeset
    22
  val PROOFS_PREFIX: String = "proofs/"
69634
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
    23
69756
1907222d974e clarified modules;
wenzelm
parents: 69671
diff changeset
    24
  def explode_name(s: String): List[String] = space_explode('/', s)
1907222d974e clarified modules;
wenzelm
parents: 69671
diff changeset
    25
  def implode_name(elems: Iterable[String]): String = elems.mkString("/")
69634
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
    26
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
    27
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    28
  /* SQL data model */
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    29
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    30
  object Data
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    31
  {
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    32
    val session_name = SQL.Column.string("session_name").make_primary_key
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    33
    val theory_name = SQL.Column.string("theory_name").make_primary_key
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    34
    val name = SQL.Column.string("name").make_primary_key
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
    35
    val executable = SQL.Column.bool("executable")
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    36
    val compressed = SQL.Column.bool("compressed")
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    37
    val body = SQL.Column.bytes("body")
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    38
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    39
    val table =
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
    40
      SQL.Table("isabelle_exports",
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
    41
        List(session_name, theory_name, name, executable, compressed, body))
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    42
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    43
    def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    44
      "WHERE " + Data.session_name.equal(session_name) +
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    45
        (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    46
        (if (name == "") "" else " AND " + Data.name.equal(name))
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    47
  }
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    48
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    49
  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    50
  {
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    51
    val select =
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    52
      Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    53
    db.using_statement(select)(stmt => stmt.execute_query().next())
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    54
  }
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    55
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    56
  def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    57
  {
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    58
    val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    59
    db.using_statement(select)(stmt =>
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    60
      stmt.execute_query().iterator(res => res.string(Data.name)).toList)
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    61
  }
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    62
68222
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    63
  def read_theory_names(db: SQL.Database, session_name: String): List[String] =
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    64
  {
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    65
    val select =
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    66
      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    67
    db.using_statement(select)(stmt =>
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    68
      stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    69
  }
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    70
3c1a716e7f59 tuned queries;
wenzelm
parents: 68221
diff changeset
    71
  def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
68115
23c6ae3dd3a0 more efficient query;
wenzelm
parents: 68104
diff changeset
    72
  {
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    73
    val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    74
    db.using_statement(select)(stmt =>
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    75
      stmt.execute_query().iterator(res =>
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    76
        (res.string(Data.theory_name), res.string(Data.name))).toList)
68115
23c6ae3dd3a0 more efficient query;
wenzelm
parents: 68104
diff changeset
    77
  }
23c6ae3dd3a0 more efficient query;
wenzelm
parents: 68104
diff changeset
    78
68104
wenzelm
parents: 68103
diff changeset
    79
  def message(msg: String, theory_name: String, name: String): String =
wenzelm
parents: 68103
diff changeset
    80
    msg + " " + quote(name) + " for theory " + quote(theory_name)
wenzelm
parents: 68103
diff changeset
    81
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    82
  def compound_name(a: String, b: String): String = a + ":" + b
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
    83
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
    84
  def empty_entry(session_name: String, theory_name: String, name: String): Entry =
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
    85
    Entry(session_name, theory_name, name, false, Future.value(false, Bytes.empty))
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
    86
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    87
  sealed case class Entry(
68103
c5764b8b2a87 more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents: 68102
diff changeset
    88
    session_name: String,
c5764b8b2a87 more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents: 68102
diff changeset
    89
    theory_name: String,
c5764b8b2a87 more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents: 68102
diff changeset
    90
    name: String,
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
    91
    executable: Boolean,
68167
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68166
diff changeset
    92
    body: Future[(Boolean, Bytes)])
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
    93
  {
69635
95dc926fa39c clarified output (again);
wenzelm
parents: 69634
diff changeset
    94
    override def toString: String = name
69630
aaa0b5f571e8 clarified output;
wenzelm
parents: 69629
diff changeset
    95
71141
b1c555d3cd71 tuned signature -- more operations;
wenzelm
parents: 71014
diff changeset
    96
    def compound_name: String = Export.compound_name(theory_name, name)
b1c555d3cd71 tuned signature -- more operations;
wenzelm
parents: 71014
diff changeset
    97
72691
2126cf946086 clarified signature;
wenzelm
parents: 72683
diff changeset
    98
    def name_has_prefix(s: String): Boolean = name.startsWith(s)
69634
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
    99
    val name_elems: List[String] = explode_name(name)
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
   100
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
   101
    def name_extends(elems: List[String]): Boolean =
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
   102
      name_elems.startsWith(elems) && name_elems != elems
70f1994988d4 more operations;
wenzelm
parents: 69630
diff changeset
   103
69630
aaa0b5f571e8 clarified output;
wenzelm
parents: 69629
diff changeset
   104
    def text: String = uncompressed().text
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   105
69629
wenzelm
parents: 68924
diff changeset
   106
    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
wenzelm
parents: 68924
diff changeset
   107
    {
wenzelm
parents: 68924
diff changeset
   108
      val (compressed, bytes) = body.join
wenzelm
parents: 68924
diff changeset
   109
      if (compressed) bytes.uncompress(cache = cache) else bytes
wenzelm
parents: 68924
diff changeset
   110
    }
wenzelm
parents: 68924
diff changeset
   111
wenzelm
parents: 68924
diff changeset
   112
    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
wenzelm
parents: 68924
diff changeset
   113
      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
wenzelm
parents: 68924
diff changeset
   114
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   115
    def write(db: SQL.Database)
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   116
    {
68167
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68166
diff changeset
   117
      val (compressed, bytes) = body.join
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   118
      db.using_statement(Data.table.insert())(stmt =>
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   119
      {
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   120
        stmt.string(1) = session_name
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   121
        stmt.string(2) = theory_name
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   122
        stmt.string(3) = name
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   123
        stmt.bool(4) = executable
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   124
        stmt.bool(5) = compressed
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   125
        stmt.bytes(6) = bytes
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   126
        stmt.execute()
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   127
      })
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   128
    }
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   129
  }
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   130
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   131
  def make_regex(pattern: String): Regex =
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   132
  {
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   133
    @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   134
      chs match {
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   135
        case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   136
        case '*' :: rest => make("[^:/]*" :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   137
        case '?' :: rest => make("[^:/]" :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   138
        case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   139
        case '{' :: rest => make("(" :: result, depth + 1, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   140
        case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   141
        case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   142
        case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   143
        case c :: rest => make(c.toString :: result, depth, rest)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   144
        case Nil => result.reverse.mkString.r
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   145
      }
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   146
    make(Nil, 0, pattern.toList)
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   147
  }
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   148
68151
wenzelm
parents: 68116
diff changeset
   149
  def make_matcher(pattern: String): (String, String) => Boolean =
wenzelm
parents: 68116
diff changeset
   150
  {
wenzelm
parents: 68116
diff changeset
   151
    val regex = make_regex(pattern)
wenzelm
parents: 68116
diff changeset
   152
    (theory_name: String, name: String) =>
wenzelm
parents: 68116
diff changeset
   153
      regex.pattern.matcher(compound_name(theory_name, name)).matches
wenzelm
parents: 68116
diff changeset
   154
  }
wenzelm
parents: 68116
diff changeset
   155
71624
f0499449e149 clarified modules;
wenzelm
parents: 71601
diff changeset
   156
  def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes,
68166
021c6fecaf5c tuned -- use XZ.Cache;
wenzelm
parents: 68151
diff changeset
   157
    cache: XZ.Cache = XZ.cache()): Entry =
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68092
diff changeset
   158
  {
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   159
    Entry(session_name, args.theory_name, args.name, args.executable,
71963
3e7d89d9912e back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
wenzelm
parents: 71939
diff changeset
   160
      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
68167
327bb0f5f768 clarified implicit compression;
wenzelm
parents: 68166
diff changeset
   161
      else Future.value((false, body)))
68101
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68092
diff changeset
   162
  }
0699a0bacc50 store exports within PIDE command state;
wenzelm
parents: 68092
diff changeset
   163
68202
a99180ad3441 clarified signature;
wenzelm
parents: 68171
diff changeset
   164
  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
a99180ad3441 clarified signature;
wenzelm
parents: 68171
diff changeset
   165
    : Option[Entry] =
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   166
  {
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   167
    val select =
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   168
      Data.table.select(List(Data.executable, Data.compressed, Data.body),
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   169
        Data.where_equal(session_name, theory_name, name))
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   170
    db.using_statement(select)(stmt =>
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   171
    {
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   172
      val res = stmt.execute_query()
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   173
      if (res.next()) {
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   174
        val executable = res.bool(Data.executable)
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   175
        val compressed = res.bool(Data.compressed)
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   176
        val body = res.bytes(Data.body)
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   177
        Some(Entry(session_name, theory_name, name, executable, Future.value(compressed, body)))
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   178
      }
68202
a99180ad3441 clarified signature;
wenzelm
parents: 68171
diff changeset
   179
      else None
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   180
    })
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   181
  }
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   182
68831
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   183
  def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] =
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   184
  {
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   185
    val path = dir + Path.basic(theory_name) + Path.explode(name)
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   186
    if (path.is_file) {
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   187
      val executable = File.is_executable(path)
68831
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   188
      val uncompressed = Bytes.read(path)
69788
c175499a7537 added executable flag for exports;
wenzelm
parents: 69756
diff changeset
   189
      Some(Entry(session_name, theory_name, name, executable, Future.value((false, uncompressed))))
68831
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   190
    }
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   191
    else None
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   192
  }
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   193
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   194
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   195
  /* database consumer thread */
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   196
68289
c29fc61fb1b1 clarified cache;
wenzelm
parents: 68288
diff changeset
   197
  def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   198
68289
c29fc61fb1b1 clarified cache;
wenzelm
parents: 68288
diff changeset
   199
  class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   200
  {
68924
wenzelm
parents: 68832
diff changeset
   201
    private val errors = Synchronized[List[String]](Nil)
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   202
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   203
    private val consumer =
71145
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   204
      Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   205
        bulk = { case (entry, _) => entry.body.is_finished },
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   206
        consume =
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   207
          (args: List[(Entry, Boolean)]) =>
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   208
          {
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   209
            val results =
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   210
              db.transaction {
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   211
                for ((entry, strict) <- args)
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   212
                yield {
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   213
                  if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   214
                    if (strict) {
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   215
                      val msg = message("Duplicate export", entry.theory_name, entry.name)
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   216
                      errors.change(msg :: _)
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   217
                    }
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   218
                    Exn.Res(())
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   219
                  }
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   220
                  else Exn.capture { entry.write(db) }
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   221
                }
70499
f389019024ce allow duplicate exports via strict = false;
wenzelm
parents: 69854
diff changeset
   222
              }
71145
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   223
            (results, true)
2f782d5f5d5a improved performance of session exports via bulk transactions;
wenzelm
parents: 71141
diff changeset
   224
          })
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   225
71624
f0499449e149 clarified modules;
wenzelm
parents: 71601
diff changeset
   226
    def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit =
70499
f389019024ce allow duplicate exports via strict = false;
wenzelm
parents: 69854
diff changeset
   227
      consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict)
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   228
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   229
    def shutdown(close: Boolean = false): List[String] =
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   230
    {
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   231
      consumer.shutdown()
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   232
      if (close) db.close()
68924
wenzelm
parents: 68832
diff changeset
   233
      errors.value.reverse
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   234
    }
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   235
  }
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   236
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   237
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   238
  /* abstract provider */
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   239
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   240
  object Provider
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   241
  {
71014
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   242
    def none: Provider =
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   243
      new Provider {
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   244
        def apply(export_name: String): Option[Entry] = None
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   245
        def focus(other_theory: String): Provider = this
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   246
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   247
        override def toString: String = "none"
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   248
      }
58022ee70b35 more operations;
wenzelm
parents: 70539
diff changeset
   249
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   250
    def database_context(
72682
e0443773ef1a clarified modules;
wenzelm
parents: 72634
diff changeset
   251
        context: Sessions.Database_Context, session: String, theory_name: String): Provider =
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   252
      new Provider {
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   253
        def apply(export_name: String): Option[Entry] =
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   254
          context.read_export(session, theory_name, export_name)
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   255
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   256
        def focus(other_theory: String): Provider = this
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   257
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   258
        override def toString: String = context.toString
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   259
      }
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72375
diff changeset
   260
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   261
    def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   262
      new Provider {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   263
        def apply(export_name: String): Option[Entry] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   264
          read_entry(db, session_name, theory_name, export_name)
68832
9b9fc9ea9dd1 tuned output;
wenzelm
parents: 68831
diff changeset
   265
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   266
        def focus(other_theory: String): Provider =
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   267
          if (other_theory == theory_name) this
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   268
          else Provider.database(db, session_name, other_theory)
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   269
68832
9b9fc9ea9dd1 tuned output;
wenzelm
parents: 68831
diff changeset
   270
        override def toString: String = db.toString
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   271
      }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   272
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   273
    def snapshot(snapshot: Document.Snapshot): Provider =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   274
      new Provider {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   275
        def apply(export_name: String): Option[Entry] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   276
          snapshot.exports_map.get(export_name)
68832
9b9fc9ea9dd1 tuned output;
wenzelm
parents: 68831
diff changeset
   277
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   278
        def focus(other_theory: String): Provider =
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   279
          if (other_theory == snapshot.node_name.theory) this
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   280
          else {
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   281
            val node_name =
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   282
              snapshot.version.nodes.theory_name(other_theory) getOrElse
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   283
                error("Bad theory " + quote(other_theory))
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   284
            Provider.snapshot(snapshot.state.snapshot(node_name))
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   285
          }
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   286
68832
9b9fc9ea9dd1 tuned output;
wenzelm
parents: 68831
diff changeset
   287
        override def toString: String = snapshot.toString
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   288
      }
68831
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   289
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   290
    def directory(dir: Path, session_name: String, theory_name: String): Provider =
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   291
      new Provider {
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   292
        def apply(export_name: String): Option[Entry] =
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   293
          read_entry(dir, session_name, theory_name, export_name)
68832
9b9fc9ea9dd1 tuned output;
wenzelm
parents: 68831
diff changeset
   294
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   295
        def focus(other_theory: String): Provider =
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   296
          if (other_theory == theory_name) this
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   297
          else Provider.directory(dir, session_name, other_theory)
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   298
68832
9b9fc9ea9dd1 tuned output;
wenzelm
parents: 68831
diff changeset
   299
        override def toString: String = dir.toString
68831
a6c69599ab99 Export.Provider for "isabelle dump" output_dir;
wenzelm
parents: 68418
diff changeset
   300
      }
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   301
  }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   302
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   303
  trait Provider
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   304
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   305
    def apply(export_name: String): Option[Entry]
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   306
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   307
    def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   308
      apply(export_name) match {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   309
        case Some(entry) => entry.uncompressed_yxml(cache = cache)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   310
        case None => Nil
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   311
      }
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   312
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70499
diff changeset
   313
    def focus(other_theory: String): Provider
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   314
  }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   315
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68331
diff changeset
   316
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   317
  /* export to file-system */
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   318
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   319
  def export_files(
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   320
    store: Sessions.Store,
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   321
    session_name: String,
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   322
    export_dir: Path,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71624
diff changeset
   323
    progress: Progress = new Progress,
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   324
    export_prune: Int = 0,
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   325
    export_list: Boolean = false,
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69789
diff changeset
   326
    export_patterns: List[String] = Nil)
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   327
  {
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   328
    using(store.open_database(session_name))(db =>
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   329
    {
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   330
      db.transaction {
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   331
        val export_names = read_theory_exports(db, session_name)
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   332
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   333
        // list
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   334
        if (export_list) {
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   335
          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71145
diff changeset
   336
            sorted.foreach(progress.echo)
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   337
        }
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   338
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   339
        // export
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   340
        if (export_patterns.nonEmpty) {
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   341
          val exports =
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   342
            (for {
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   343
              export_pattern <- export_patterns.iterator
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   344
              matcher = make_matcher(export_pattern)
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   345
              (theory_name, name) <- export_names if matcher(theory_name, name)
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   346
            } yield (theory_name, name)).toSet
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   347
          for {
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   348
            (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   349
            name <- group.map(_._2).sorted
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   350
            entry <- read_entry(db, session_name, theory_name, name)
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   351
          } {
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   352
            val elems = theory_name :: space_explode('/', name)
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   353
            val path =
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   354
              if (elems.length < export_prune + 1) {
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   355
                error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   356
              }
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   357
              else export_dir + Path.make(elems.drop(export_prune))
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   358
69811
18f61ce86425 clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents: 69789
diff changeset
   359
            progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71963
diff changeset
   360
            Isabelle_System.make_directory(path.dir)
68289
c29fc61fb1b1 clarified cache;
wenzelm
parents: 68288
diff changeset
   361
            Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
69789
2c3e5e58d93f more thorough File.set_executable, notably for Windows;
wenzelm
parents: 69788
diff changeset
   362
            File.set_executable(path, entry.executable)
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   363
          }
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   364
        }
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   365
      }
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   366
    })
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   367
  }
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   368
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   369
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   370
  /* Isabelle tool wrapper */
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   371
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71145
diff changeset
   372
  val default_export_dir: Path = Path.explode("export")
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   373
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   374
  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   375
  {
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   376
    /* arguments */
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   377
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   378
    var export_dir = default_export_dir
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   379
    var dirs: List[Path] = Nil
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   380
    var export_list = false
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   381
    var no_build = false
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   382
    var options = Options.init()
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   383
    var export_prune = 0
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   384
    var export_patterns: List[String] = Nil
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   385
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   386
    val getopts = Getopts("""
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   387
Usage: isabelle export [OPTIONS] SESSION
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   388
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   389
  Options are:
68314
2acbf8129d8b clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents: 68305
diff changeset
   390
    -O DIR       output directory for exported files (default: """ + default_export_dir + """)
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   391
    -d DIR       include session directory
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   392
    -l           list exports
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   393
    -n           no build of session
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   394
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   395
    -p NUM       prune path of exported files by NUM elements
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   396
    -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   397
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   398
  List or export theory exports for SESSION: named blobs produced by
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   399
  isabelle build. Option -l or -x is required; option -x may be repeated.
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   400
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   401
  The PATTERN language resembles glob patterns in the shell, with ? and *
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   402
  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   403
  and variants {pattern1,pattern2,pattern3}.
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   404
""",
68314
2acbf8129d8b clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents: 68305
diff changeset
   405
      "O:" -> (arg => export_dir = Path.explode(arg)),
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   406
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   407
      "l" -> (_ => export_list = true),
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   408
      "n" -> (_ => no_build = true),
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   409
      "o:" -> (arg => options = options + arg),
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   410
      "p:" -> (arg => export_prune = Value.Int.parse(arg)),
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   411
      "x:" -> (arg => export_patterns ::= arg))
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   412
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   413
    val more_args = getopts(args)
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   414
    val session_name =
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   415
      more_args match {
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   416
        case List(session_name) if export_list || export_patterns.nonEmpty => session_name
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   417
        case _ => getopts.usage()
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   418
      }
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   419
68305
5321218147d3 clarified signature;
wenzelm
parents: 68291
diff changeset
   420
    val progress = new Console_Progress()
5321218147d3 clarified signature;
wenzelm
parents: 68291
diff changeset
   421
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   422
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   423
    /* build */
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   424
68305
5321218147d3 clarified signature;
wenzelm
parents: 68291
diff changeset
   425
    if (!no_build) {
5321218147d3 clarified signature;
wenzelm
parents: 68291
diff changeset
   426
      val rc =
68331
7eaaa8f48331 clarified outermost progress.interrupt_handler;
wenzelm
parents: 68314
diff changeset
   427
        progress.interrupt_handler {
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69811
diff changeset
   428
          Build.build_logic(options, session_name, progress = progress, dirs = dirs)
68331
7eaaa8f48331 clarified outermost progress.interrupt_handler;
wenzelm
parents: 68314
diff changeset
   429
        }
68305
5321218147d3 clarified signature;
wenzelm
parents: 68291
diff changeset
   430
      if (rc != 0) sys.exit(rc)
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   431
    }
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   432
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   433
68288
d20770229f99 tuned signature;
wenzelm
parents: 68222
diff changeset
   434
    /* export files */
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   435
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69811
diff changeset
   436
    val store = Sessions.store(options)
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69635
diff changeset
   437
    export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
68290
f1f5ccc85b25 support multiple patterns;
wenzelm
parents: 68289
diff changeset
   438
      export_list = export_list, export_patterns = export_patterns)
68116
ac82ee617a75 command-line tool "isabelle export";
wenzelm
parents: 68115
diff changeset
   439
  })
68092
888d35a19866 store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff changeset
   440
}