author | wenzelm |
Fri, 11 May 2018 20:22:20 +0200 | |
changeset 68151 | 3c321783bae3 |
parent 68116 | ac82ee617a75 |
child 68166 | 021c6fecaf5c |
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 |
|
68116 | 49 |
def read_theory_names(db: SQL.Database, session_name: String): List[(String, String)] = |
68115 | 50 |
{ |
68116 | 51 |
val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) |
52 |
db.using_statement(select)(stmt => |
|
53 |
stmt.execute_query().iterator(res => |
|
54 |
(res.string(Data.theory_name), res.string(Data.name))).toList) |
|
68115 | 55 |
} |
56 |
||
68104 | 57 |
def message(msg: String, theory_name: String, name: String): String = |
58 |
msg + " " + quote(name) + " for theory " + quote(theory_name) |
|
59 |
||
68116 | 60 |
def compound_name(a: String, b: String): String = a + ":" + b |
61 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
62 |
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
|
63 |
session_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
64 |
theory_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
65 |
name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
66 |
compressed: Boolean, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
67 |
body: Future[Bytes]) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
68 |
{ |
68116 | 69 |
override def toString: String = compound_name(theory_name, name) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
70 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
71 |
def write(db: SQL.Database) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
72 |
{ |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
73 |
val bytes = body.join |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
74 |
db.using_statement(Data.table.insert())(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
75 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
76 |
stmt.string(1) = session_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
77 |
stmt.string(2) = theory_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
78 |
stmt.string(3) = name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
79 |
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
|
80 |
stmt.bytes(5) = bytes |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
81 |
stmt.execute() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
82 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
83 |
} |
68116 | 84 |
|
85 |
def body_uncompressed: Bytes = |
|
86 |
if (compressed) body.join.uncompress() else body.join |
|
87 |
} |
|
88 |
||
89 |
def make_regex(pattern: String): Regex = |
|
90 |
{ |
|
91 |
@tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = |
|
92 |
chs match { |
|
93 |
case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) |
|
94 |
case '*' :: rest => make("[^:/]*" :: result, depth, rest) |
|
95 |
case '?' :: rest => make("[^:/]" :: result, depth, rest) |
|
96 |
case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) |
|
97 |
case '{' :: rest => make("(" :: result, depth + 1, rest) |
|
98 |
case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) |
|
99 |
case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) |
|
100 |
case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) |
|
101 |
case c :: rest => make(c.toString :: result, depth, rest) |
|
102 |
case Nil => result.reverse.mkString.r |
|
103 |
} |
|
104 |
make(Nil, 0, pattern.toList) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
105 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
106 |
|
68151 | 107 |
def make_matcher(pattern: String): (String, String) => Boolean = |
108 |
{ |
|
109 |
val regex = make_regex(pattern) |
|
110 |
(theory_name: String, name: String) => |
|
111 |
regex.pattern.matcher(compound_name(theory_name, name)).matches |
|
112 |
} |
|
113 |
||
68101 | 114 |
def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry = |
115 |
{ |
|
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
116 |
Entry(session_name, args.theory_name, args.name, args.compress, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
117 |
if (args.compress) Future.fork(body.compress()) else Future.value(body)) |
68101 | 118 |
} |
119 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
120 |
def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
121 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
122 |
val select = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
123 |
Data.table.select(List(Data.compressed, Data.body), |
68116 | 124 |
Data.where_equal(session_name, theory_name, name)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
125 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
126 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
127 |
val res = stmt.execute_query() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
128 |
if (res.next()) { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
129 |
val compressed = res.bool(Data.compressed) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
130 |
val body = res.bytes(Data.body) |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
131 |
Entry(session_name, theory_name, name, compressed, Future.value(body)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
132 |
} |
68104 | 133 |
else error(message("Bad export", theory_name, name)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
134 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
135 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
136 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
137 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
138 |
/* database consumer thread */ |
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 |
def consumer(db: SQL.Database): Consumer = new Consumer(db) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
141 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
142 |
class Consumer private[Export](db: SQL.Database) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
143 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
144 |
db.create_table(Data.table) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
145 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
146 |
private val export_errors = Synchronized[List[String]](Nil) |
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 |
private val consumer = |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
149 |
Consumer_Thread.fork(name = "export")(consume = (entry: Entry) => |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
150 |
{ |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
151 |
entry.body.join |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
152 |
db.transaction { |
68115 | 153 |
if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { |
68104 | 154 |
val err = message("Duplicate export", entry.theory_name, entry.name) |
155 |
export_errors.change(errs => err :: errs) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
156 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
157 |
else entry.write(db) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
158 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
159 |
true |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
160 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
161 |
|
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
162 |
def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
163 |
consumer.send(make_entry(session_name, args, body)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
164 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
165 |
def shutdown(close: Boolean = false): List[String] = |
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 |
consumer.shutdown() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
168 |
if (close) db.close() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
169 |
export_errors.value.reverse |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
170 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
171 |
} |
68116 | 172 |
|
173 |
||
174 |
/* Isabelle tool wrapper */ |
|
175 |
||
176 |
val default_export_dir = Path.explode("export") |
|
177 |
||
178 |
val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args => |
|
179 |
{ |
|
180 |
/* arguments */ |
|
181 |
||
182 |
var export_dir = default_export_dir |
|
183 |
var dirs: List[Path] = Nil |
|
184 |
var export_list = false |
|
185 |
var no_build = false |
|
186 |
var options = Options.init() |
|
187 |
var system_mode = false |
|
188 |
var export_pattern = "" |
|
189 |
||
190 |
val getopts = Getopts(""" |
|
191 |
Usage: isabelle export [OPTIONS] SESSION |
|
192 |
||
193 |
Options are: |
|
194 |
-D DIR target directory for exported files (default: """ + default_export_dir + """) |
|
195 |
-d DIR include session directory |
|
196 |
-l list exports |
|
197 |
-n no build of session |
|
198 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
199 |
-s system build mode for session image |
|
200 |
-x PATTERN extract files matching pattern (e.g. "*:**" for all) |
|
201 |
||
202 |
List or export theory exports for SESSION: named blobs produced by |
|
203 |
isabelle build. Option -l or -x is required. |
|
204 |
||
205 |
The PATTERN language resembles glob patterns in the shell, with ? and * |
|
206 |
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], |
|
207 |
and variants {pattern1,pattern2,pattern3}. |
|
208 |
""", |
|
209 |
"D:" -> (arg => export_dir = Path.explode(arg)), |
|
210 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
211 |
"l" -> (_ => export_list = true), |
|
212 |
"n" -> (_ => no_build = true), |
|
213 |
"o:" -> (arg => options = options + arg), |
|
214 |
"s" -> (_ => system_mode = true), |
|
215 |
"x:" -> (arg => export_pattern = arg)) |
|
216 |
||
217 |
val more_args = getopts(args) |
|
218 |
val session_name = |
|
219 |
more_args match { |
|
220 |
case List(session_name) if export_list || export_pattern != "" => session_name |
|
221 |
case _ => getopts.usage() |
|
222 |
} |
|
223 |
||
224 |
||
225 |
/* build */ |
|
226 |
||
227 |
val progress = new Console_Progress() |
|
228 |
||
229 |
if (!no_build && |
|
230 |
!Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode, |
|
231 |
sessions = List(session_name)).ok) |
|
232 |
{ |
|
233 |
progress.echo("Build started for Isabelle/" + session_name + " ...") |
|
234 |
progress.interrupt_handler { |
|
235 |
val res = |
|
236 |
Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode, |
|
237 |
sessions = List(session_name)) |
|
238 |
if (!res.ok) sys.exit(res.rc) |
|
239 |
} |
|
240 |
} |
|
241 |
||
242 |
||
243 |
/* database */ |
|
244 |
||
245 |
val store = Sessions.store(system_mode) |
|
246 |
val database = |
|
247 |
store.find_database(session_name) match { |
|
248 |
case None => error("Missing database for session " + quote(session_name)) |
|
249 |
case Some(database) => database |
|
250 |
} |
|
251 |
||
252 |
using(SQLite.open_database(database))(db => |
|
253 |
{ |
|
254 |
db.transaction { |
|
255 |
val export_names = read_theory_names(db, session_name) |
|
256 |
||
257 |
// list |
|
258 |
if (export_list) { |
|
259 |
(for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). |
|
260 |
sorted.foreach(Output.writeln(_, stdout = true)) |
|
261 |
} |
|
262 |
||
263 |
// export |
|
264 |
if (export_pattern != "") { |
|
68151 | 265 |
val matcher = make_matcher(export_pattern) |
266 |
for { (theory_name, name) <- export_names if matcher(theory_name, name) } |
|
267 |
{ |
|
68116 | 268 |
val entry = read_entry(db, session_name, theory_name, name) |
269 |
val path = export_dir + Path.basic(theory_name) + Path.explode(name) |
|
270 |
||
271 |
progress.echo("exporting " + path) |
|
272 |
Isabelle_System.mkdirs(path.dir) |
|
273 |
Bytes.write(path, entry.body_uncompressed) |
|
274 |
} |
|
275 |
} |
|
276 |
} |
|
277 |
}) |
|
278 |
}) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
279 |
} |