author | wenzelm |
Fri, 11 Jan 2019 11:35:16 +0100 | |
changeset 69630 | aaa0b5f571e8 |
parent 69629 | e1188d9d616b |
child 69634 | 70f1994988d4 |
permissions | -rw-r--r-- |
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 | 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 | 9 |
|
10 |
import scala.annotation.tailrec |
|
11 |
import scala.util.matching.Regex |
|
12 |
||
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 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
16 |
/* SQL data model */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
17 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
18 |
object Data |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
19 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
20 |
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
|
21 |
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
|
22 |
val name = SQL.Column.string("name").make_primary_key |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
23 |
val compressed = SQL.Column.bool("compressed") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
24 |
val body = SQL.Column.bytes("body") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
25 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
26 |
val table = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
27 |
SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body)) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
28 |
|
68116 | 29 |
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
|
30 |
"WHERE " + Data.session_name.equal(session_name) + |
68116 | 31 |
(if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) + |
32 |
(if (name == "") "" else " AND " + Data.name.equal(name)) |
|
33 |
} |
|
34 |
||
35 |
def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean = |
|
36 |
{ |
|
37 |
val select = |
|
38 |
Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name)) |
|
39 |
db.using_statement(select)(stmt => stmt.execute_query().next()) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
40 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
41 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
42 |
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
|
43 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
44 |
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
|
45 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
46 |
stmt.execute_query().iterator(res => res.string(Data.name)).toList) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
47 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
48 |
|
68222 | 49 |
def read_theory_names(db: SQL.Database, session_name: String): List[String] = |
50 |
{ |
|
51 |
val select = |
|
52 |
Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) |
|
53 |
db.using_statement(select)(stmt => |
|
54 |
stmt.execute_query().iterator(_.string(Data.theory_name)).toList) |
|
55 |
} |
|
56 |
||
57 |
def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] = |
|
68115 | 58 |
{ |
68116 | 59 |
val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) |
60 |
db.using_statement(select)(stmt => |
|
61 |
stmt.execute_query().iterator(res => |
|
62 |
(res.string(Data.theory_name), res.string(Data.name))).toList) |
|
68115 | 63 |
} |
64 |
||
68104 | 65 |
def message(msg: String, theory_name: String, name: String): String = |
66 |
msg + " " + quote(name) + " for theory " + quote(theory_name) |
|
67 |
||
68116 | 68 |
def compound_name(a: String, b: String): String = a + ":" + b |
69 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
70 |
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
|
71 |
session_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
72 |
theory_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
73 |
name: String, |
68167 | 74 |
body: Future[(Boolean, Bytes)]) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
75 |
{ |
69630 | 76 |
override def toString: String = uncompressed().toString |
77 |
||
78 |
def text: String = uncompressed().text |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
79 |
|
69629 | 80 |
def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes = |
81 |
{ |
|
82 |
val (compressed, bytes) = body.join |
|
83 |
if (compressed) bytes.uncompress(cache = cache) else bytes |
|
84 |
} |
|
85 |
||
86 |
def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body = |
|
87 |
YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache))) |
|
88 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
89 |
def write(db: SQL.Database) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
90 |
{ |
68167 | 91 |
val (compressed, bytes) = body.join |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
92 |
db.using_statement(Data.table.insert())(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
93 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
94 |
stmt.string(1) = session_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
95 |
stmt.string(2) = theory_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
96 |
stmt.string(3) = name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
97 |
stmt.bool(4) = compressed |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
98 |
stmt.bytes(5) = bytes |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
99 |
stmt.execute() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
100 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
101 |
} |
68116 | 102 |
} |
103 |
||
104 |
def make_regex(pattern: String): Regex = |
|
105 |
{ |
|
106 |
@tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = |
|
107 |
chs match { |
|
108 |
case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) |
|
109 |
case '*' :: rest => make("[^:/]*" :: result, depth, rest) |
|
110 |
case '?' :: rest => make("[^:/]" :: result, depth, rest) |
|
111 |
case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) |
|
112 |
case '{' :: rest => make("(" :: result, depth + 1, rest) |
|
113 |
case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) |
|
114 |
case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) |
|
115 |
case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) |
|
116 |
case c :: rest => make(c.toString :: result, depth, rest) |
|
117 |
case Nil => result.reverse.mkString.r |
|
118 |
} |
|
119 |
make(Nil, 0, pattern.toList) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
120 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
121 |
|
68151 | 122 |
def make_matcher(pattern: String): (String, String) => Boolean = |
123 |
{ |
|
124 |
val regex = make_regex(pattern) |
|
125 |
(theory_name: String, name: String) => |
|
126 |
regex.pattern.matcher(compound_name(theory_name, name)).matches |
|
127 |
} |
|
128 |
||
68166 | 129 |
def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes, |
130 |
cache: XZ.Cache = XZ.cache()): Entry = |
|
68101 | 131 |
{ |
68167 | 132 |
Entry(session_name, args.theory_name, args.name, |
133 |
if (args.compress) Future.fork(body.maybe_compress(cache = cache)) |
|
134 |
else Future.value((false, body))) |
|
68101 | 135 |
} |
136 |
||
68202 | 137 |
def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String) |
138 |
: Option[Entry] = |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
139 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
140 |
val select = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
141 |
Data.table.select(List(Data.compressed, Data.body), |
68116 | 142 |
Data.where_equal(session_name, theory_name, name)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
143 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
144 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
145 |
val res = stmt.execute_query() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
146 |
if (res.next()) { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
147 |
val compressed = res.bool(Data.compressed) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
148 |
val body = res.bytes(Data.body) |
68202 | 149 |
Some(Entry(session_name, theory_name, name, Future.value(compressed, body))) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
150 |
} |
68202 | 151 |
else None |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
152 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
153 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
154 |
|
68831 | 155 |
def read_entry(dir: Path, session_name: String, theory_name: String, name: String): Option[Entry] = |
156 |
{ |
|
157 |
val path = dir + Path.basic(theory_name) + Path.explode(name) |
|
158 |
if (path.is_file) { |
|
159 |
val uncompressed = Bytes.read(path) |
|
160 |
Some(Entry(session_name, theory_name, name, Future.value((false, uncompressed)))) |
|
161 |
} |
|
162 |
else None |
|
163 |
} |
|
164 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
165 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
166 |
/* database consumer thread */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
167 |
|
68289 | 168 |
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
|
169 |
|
68289 | 170 |
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
|
171 |
{ |
68924 | 172 |
private val errors = Synchronized[List[String]](Nil) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
173 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
174 |
private val consumer = |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
175 |
Consumer_Thread.fork(name = "export")(consume = (entry: Entry) => |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
176 |
{ |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
177 |
entry.body.join |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
178 |
db.transaction { |
68115 | 179 |
if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { |
68924 | 180 |
val msg = message("Duplicate export", entry.theory_name, entry.name) |
181 |
errors.change(msg :: _) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
182 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
183 |
else entry.write(db) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
184 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
185 |
true |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
186 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
187 |
|
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
188 |
def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = |
68289 | 189 |
consumer.send(make_entry(session_name, args, body, cache = cache)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
190 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
191 |
def shutdown(close: Boolean = false): List[String] = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
192 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
193 |
consumer.shutdown() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
194 |
if (close) db.close() |
68924 | 195 |
errors.value.reverse |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
196 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
197 |
} |
68116 | 198 |
|
199 |
||
68418 | 200 |
/* abstract provider */ |
201 |
||
202 |
object Provider |
|
203 |
{ |
|
204 |
def database(db: SQL.Database, session_name: String, theory_name: String): Provider = |
|
205 |
new Provider { |
|
206 |
def apply(export_name: String): Option[Entry] = |
|
207 |
read_entry(db, session_name, theory_name, export_name) |
|
68832 | 208 |
|
209 |
override def toString: String = db.toString |
|
68418 | 210 |
} |
211 |
||
212 |
def snapshot(snapshot: Document.Snapshot): Provider = |
|
213 |
new Provider { |
|
214 |
def apply(export_name: String): Option[Entry] = |
|
215 |
snapshot.exports_map.get(export_name) |
|
68832 | 216 |
|
217 |
override def toString: String = snapshot.toString |
|
68418 | 218 |
} |
68831 | 219 |
|
220 |
def directory(dir: Path, session_name: String, theory_name: String): Provider = |
|
221 |
new Provider { |
|
222 |
def apply(export_name: String): Option[Entry] = |
|
223 |
read_entry(dir, session_name, theory_name, export_name) |
|
68832 | 224 |
|
225 |
override def toString: String = dir.toString |
|
68831 | 226 |
} |
68418 | 227 |
} |
228 |
||
229 |
trait Provider |
|
230 |
{ |
|
231 |
def apply(export_name: String): Option[Entry] |
|
232 |
||
233 |
def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body = |
|
234 |
apply(export_name) match { |
|
235 |
case Some(entry) => entry.uncompressed_yxml(cache = cache) |
|
236 |
case None => Nil |
|
237 |
} |
|
238 |
} |
|
239 |
||
240 |
||
68288 | 241 |
/* export to file-system */ |
242 |
||
243 |
def export_files( |
|
244 |
store: Sessions.Store, |
|
245 |
session_name: String, |
|
246 |
export_dir: Path, |
|
247 |
progress: Progress = No_Progress, |
|
248 |
export_list: Boolean = false, |
|
68291 | 249 |
export_patterns: List[String] = Nil, |
250 |
export_prefix: String = "") |
|
68288 | 251 |
{ |
252 |
using(store.open_database(session_name))(db => |
|
253 |
{ |
|
254 |
db.transaction { |
|
255 |
val export_names = read_theory_exports(db, session_name) |
|
256 |
||
257 |
// list |
|
258 |
if (export_list) { |
|
259 |
(for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). |
|
68291 | 260 |
sorted.foreach(progress.echo(_)) |
68288 | 261 |
} |
262 |
||
263 |
// export |
|
68290 | 264 |
if (export_patterns.nonEmpty) { |
265 |
val exports = |
|
266 |
(for { |
|
267 |
export_pattern <- export_patterns.iterator |
|
268 |
matcher = make_matcher(export_pattern) |
|
269 |
(theory_name, name) <- export_names if matcher(theory_name, name) |
|
270 |
} yield (theory_name, name)).toSet |
|
68288 | 271 |
for { |
68290 | 272 |
(theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1) |
273 |
name <- group.map(_._2).sorted |
|
68288 | 274 |
entry <- read_entry(db, session_name, theory_name, name) |
275 |
} { |
|
276 |
val path = export_dir + Path.basic(theory_name) + Path.explode(name) |
|
68291 | 277 |
progress.echo(export_prefix + "export " + path) |
68288 | 278 |
Isabelle_System.mkdirs(path.dir) |
68289 | 279 |
Bytes.write(path, entry.uncompressed(cache = store.xz_cache)) |
68288 | 280 |
} |
281 |
} |
|
282 |
} |
|
283 |
}) |
|
284 |
} |
|
285 |
||
286 |
||
68116 | 287 |
/* Isabelle tool wrapper */ |
288 |
||
289 |
val default_export_dir = Path.explode("export") |
|
290 |
||
291 |
val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args => |
|
292 |
{ |
|
293 |
/* arguments */ |
|
294 |
||
295 |
var export_dir = default_export_dir |
|
296 |
var dirs: List[Path] = Nil |
|
297 |
var export_list = false |
|
298 |
var no_build = false |
|
299 |
var options = Options.init() |
|
300 |
var system_mode = false |
|
68290 | 301 |
var export_patterns: List[String] = Nil |
68116 | 302 |
|
303 |
val getopts = Getopts(""" |
|
304 |
Usage: isabelle export [OPTIONS] SESSION |
|
305 |
||
306 |
Options are: |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68305
diff
changeset
|
307 |
-O DIR output directory for exported files (default: """ + default_export_dir + """) |
68116 | 308 |
-d DIR include session directory |
309 |
-l list exports |
|
310 |
-n no build of session |
|
311 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
312 |
-s system build mode for session image |
|
313 |
-x PATTERN extract files matching pattern (e.g. "*:**" for all) |
|
314 |
||
315 |
List or export theory exports for SESSION: named blobs produced by |
|
68290 | 316 |
isabelle build. Option -l or -x is required; option -x may be repeated. |
68116 | 317 |
|
318 |
The PATTERN language resembles glob patterns in the shell, with ? and * |
|
319 |
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], |
|
320 |
and variants {pattern1,pattern2,pattern3}. |
|
321 |
""", |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68305
diff
changeset
|
322 |
"O:" -> (arg => export_dir = Path.explode(arg)), |
68116 | 323 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
324 |
"l" -> (_ => export_list = true), |
|
325 |
"n" -> (_ => no_build = true), |
|
326 |
"o:" -> (arg => options = options + arg), |
|
327 |
"s" -> (_ => system_mode = true), |
|
68290 | 328 |
"x:" -> (arg => export_patterns ::= arg)) |
68116 | 329 |
|
330 |
val more_args = getopts(args) |
|
331 |
val session_name = |
|
332 |
more_args match { |
|
68290 | 333 |
case List(session_name) if export_list || export_patterns.nonEmpty => session_name |
68116 | 334 |
case _ => getopts.usage() |
335 |
} |
|
336 |
||
68305 | 337 |
val progress = new Console_Progress() |
338 |
||
68116 | 339 |
|
340 |
/* build */ |
|
341 |
||
68305 | 342 |
if (!no_build) { |
343 |
val rc = |
|
68331 | 344 |
progress.interrupt_handler { |
345 |
Build.build_logic(options, session_name, progress = progress, |
|
346 |
dirs = dirs, system_mode = system_mode) |
|
347 |
} |
|
68305 | 348 |
if (rc != 0) sys.exit(rc) |
68116 | 349 |
} |
350 |
||
351 |
||
68288 | 352 |
/* export files */ |
68116 | 353 |
|
68209 | 354 |
val store = Sessions.store(options, system_mode) |
68288 | 355 |
export_files(store, session_name, export_dir, progress = progress, |
68290 | 356 |
export_list = export_list, export_patterns = export_patterns) |
68116 | 357 |
}) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
358 |
} |