author | wenzelm |
Thu, 16 Mar 2023 16:28:21 +0100 | |
changeset 77681 | 1db732e6c3d2 |
parent 77599 | 2b4e5861f882 |
child 78153 | 55a6aa77f3d8 |
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 |
||
75393 | 14 |
object Export { |
72691 | 15 |
/* artefact names */ |
16 |
||
72844 | 17 |
val DOCUMENT_ID = "PIDE/document_id" |
18 |
val FILES = "PIDE/files" |
|
72702 | 19 |
val MARKUP = "PIDE/markup" |
20 |
val MESSAGES = "PIDE/messages" |
|
72691 | 21 |
val DOCUMENT_PREFIX = "document/" |
73785 | 22 |
val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex" |
72691 | 23 |
val THEORY_PREFIX: String = "theory/" |
24 |
val PROOFS_PREFIX: String = "proofs/" |
|
69634 | 25 |
|
69756 | 26 |
def explode_name(s: String): List[String] = space_explode('/', s) |
27 |
def implode_name(elems: Iterable[String]): String = elems.mkString("/") |
|
69634 | 28 |
|
29 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
30 |
/* SQL data model */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
31 |
|
75393 | 32 |
object Data { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
33 |
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
|
34 |
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
|
35 |
val name = SQL.Column.string("name").make_primary_key |
69788 | 36 |
val executable = SQL.Column.bool("executable") |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
37 |
val compressed = SQL.Column.bool("compressed") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
38 |
val body = SQL.Column.bytes("body") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
39 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
40 |
val table = |
69788 | 41 |
SQL.Table("isabelle_exports", |
42 |
List(session_name, theory_name, name, executable, compressed, body)) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
43 |
|
77599 | 44 |
val tables = SQL.Tables(table) |
45 |
||
68116 | 46 |
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = |
77370 | 47 |
SQL.where( |
48 |
SQL.and( |
|
49 |
Data.session_name.equal(session_name), |
|
50 |
if_proper(theory_name, Data.theory_name.equal(theory_name)), |
|
51 |
if_proper(name, Data.name.equal(name)))) |
|
68116 | 52 |
} |
53 |
||
75674 | 54 |
def compound_name(a: String, b: String): String = |
55 |
if (a.isEmpty) b else a + ":" + b |
|
56 |
||
75672 | 57 |
sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") { |
75674 | 58 |
val compound_name: String = Export.compound_name(theory, name) |
59 |
||
75680 | 60 |
def make_path(prune: Int = 0): Path = { |
75675 | 61 |
val elems = theory :: space_explode('/', name) |
62 |
if (elems.length < prune + 1) { |
|
63 |
error("Cannot prune path by " + prune + " element(s): " + Path.make(elems)) |
|
64 |
} |
|
75680 | 65 |
else Path.make(elems.drop(prune)) |
75675 | 66 |
} |
67 |
||
75671 | 68 |
def readable(db: SQL.Database): Boolean = { |
77552 | 69 |
db.execute_query_statementB( |
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
70 |
Data.table.select(List(Data.name), |
77552 | 71 |
sql = Data.where_equal(session, theory, name))) |
75671 | 72 |
} |
73 |
||
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
74 |
def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = |
77552 | 75 |
db.execute_query_statementO[Entry]( |
75671 | 76 |
Data.table.select(List(Data.executable, Data.compressed, Data.body), |
77552 | 77 |
sql = Data.where_equal(session, theory, name)), |
78 |
{ res => |
|
75671 | 79 |
val executable = res.bool(Data.executable) |
80 |
val compressed = res.bool(Data.compressed) |
|
81 |
val bytes = res.bytes(Data.body) |
|
82 |
val body = Future.value(compressed, bytes) |
|
77544 | 83 |
Entry(this, executable, body, cache) |
77552 | 84 |
} |
85 |
) |
|
68222 | 86 |
} |
87 |
||
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
88 |
def read_theory_names(db: SQL.Database, session_name: String): List[String] = |
77552 | 89 |
db.execute_query_statement( |
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
90 |
Data.table.select(List(Data.theory_name), distinct = true, |
77552 | 91 |
sql = Data.where_equal(session_name) + SQL.order_by(List(Data.theory_name))), |
92 |
List.from[String], res => res.string(Data.theory_name)) |
|
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
93 |
|
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
94 |
def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = |
77552 | 95 |
db.execute_query_statement( |
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77370
diff
changeset
|
96 |
Data.table.select(List(Data.theory_name, Data.name), |
77552 | 97 |
sql = Data.where_equal(session_name)) + SQL.order_by(List(Data.theory_name, Data.name)), |
98 |
List.from[Entry_Name], |
|
99 |
{ res => |
|
100 |
Entry_Name( |
|
101 |
session = session_name, |
|
102 |
theory = res.string(Data.theory_name), |
|
103 |
name = res.string(Data.name)) |
|
104 |
}) |
|
68115 | 105 |
|
68104 | 106 |
def message(msg: String, theory_name: String, name: String): String = |
107 |
msg + " " + quote(name) + " for theory " + quote(theory_name) |
|
108 |
||
76851 | 109 |
object Entry { |
110 |
def apply( |
|
111 |
entry_name: Entry_Name, |
|
112 |
executable: Boolean, |
|
113 |
body: Future[(Boolean, Bytes)], |
|
114 |
cache: XML.Cache |
|
115 |
): Entry = new Entry(entry_name, executable, body, cache) |
|
116 |
||
117 |
def empty(theory_name: String, name: String): Entry = |
|
118 |
Entry(Entry_Name(theory = theory_name, name = name), |
|
119 |
false, Future.value(false, Bytes.empty), XML.Cache.none) |
|
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
120 |
|
76851 | 121 |
def make( |
122 |
session_name: String, |
|
123 |
args: Protocol.Export.Args, |
|
124 |
bytes: Bytes, |
|
125 |
cache: XML.Cache |
|
126 |
): Entry = { |
|
127 |
val body = |
|
128 |
if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress)) |
|
129 |
else Future.value((false, bytes)) |
|
130 |
val entry_name = |
|
131 |
Entry_Name(session = session_name, theory = args.theory_name, name = args.name) |
|
132 |
Entry(entry_name, args.executable, body, cache) |
|
133 |
} |
|
134 |
} |
|
135 |
||
136 |
final class Entry private( |
|
137 |
val entry_name: Entry_Name, |
|
138 |
val executable: Boolean, |
|
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
139 |
body: Future[(Boolean, Bytes)], |
75393 | 140 |
cache: XML.Cache |
141 |
) { |
|
75671 | 142 |
def session_name: String = entry_name.session |
143 |
def theory_name: String = entry_name.theory |
|
144 |
def name: String = entry_name.name |
|
69635 | 145 |
override def toString: String = name |
69630 | 146 |
|
76851 | 147 |
def is_finished: Boolean = body.is_finished |
148 |
def cancel(): Unit = body.cancel() |
|
149 |
||
75674 | 150 |
def compound_name: String = entry_name.compound_name |
71141 | 151 |
|
72691 | 152 |
def name_has_prefix(s: String): Boolean = name.startsWith(s) |
69634 | 153 |
val name_elems: List[String] = explode_name(name) |
154 |
||
155 |
def name_extends(elems: List[String]): Boolean = |
|
156 |
name_elems.startsWith(elems) && name_elems != elems |
|
157 |
||
76852 | 158 |
def bytes: Bytes = { |
159 |
val (compressed, bs) = body.join |
|
160 |
if (compressed) bs.uncompress(cache = cache.compress) else bs |
|
69629 | 161 |
} |
162 |
||
76852 | 163 |
def text: String = bytes.text |
164 |
||
165 |
def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache) |
|
69629 | 166 |
|
75393 | 167 |
def write(db: SQL.Database): Unit = { |
76852 | 168 |
val (compressed, bs) = body.join |
77541 | 169 |
db.execute_statement(Data.table.insert(), body = |
170 |
{ stmt => |
|
171 |
stmt.string(1) = session_name |
|
172 |
stmt.string(2) = theory_name |
|
173 |
stmt.string(3) = name |
|
174 |
stmt.bool(4) = executable |
|
175 |
stmt.bool(5) = compressed |
|
176 |
stmt.bytes(6) = bs |
|
177 |
}) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
178 |
} |
68116 | 179 |
} |
180 |
||
75393 | 181 |
def make_regex(pattern: String): Regex = { |
68116 | 182 |
@tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = |
183 |
chs match { |
|
184 |
case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) |
|
185 |
case '*' :: rest => make("[^:/]*" :: result, depth, rest) |
|
186 |
case '?' :: rest => make("[^:/]" :: result, depth, rest) |
|
187 |
case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) |
|
188 |
case '{' :: rest => make("(" :: result, depth + 1, rest) |
|
189 |
case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) |
|
190 |
case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) |
|
191 |
case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) |
|
192 |
case c :: rest => make(c.toString :: result, depth, rest) |
|
193 |
case Nil => result.reverse.mkString.r |
|
194 |
} |
|
195 |
make(Nil, 0, pattern.toList) |
|
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 |
|
75674 | 198 |
def make_matcher(pats: List[String]): Entry_Name => Boolean = { |
75658
5905c7f484b3
clarified signature: read_theory_exports is already ordered;
wenzelm
parents:
75394
diff
changeset
|
199 |
val regs = pats.map(make_regex) |
76098 | 200 |
(entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name)) |
68151 | 201 |
} |
202 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
203 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
204 |
/* database consumer thread */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
205 |
|
74255 | 206 |
def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer = |
207 |
new Consumer(db, cache, progress) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
208 |
|
75393 | 209 |
class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress) { |
68924 | 210 |
private val errors = Synchronized[List[String]](Nil) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
211 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
212 |
private val consumer = |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
213 |
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")( |
76851 | 214 |
bulk = { case (entry, _) => entry.is_finished }, |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
215 |
consume = |
75394 | 216 |
{ (args: List[(Entry, Boolean)]) => |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
217 |
val results = |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
218 |
db.transaction { |
74256 | 219 |
for ((entry, strict) <- args) |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
220 |
yield { |
74257 | 221 |
if (progress.stopped) { |
76851 | 222 |
entry.cancel() |
74257 | 223 |
Exn.Res(()) |
224 |
} |
|
75671 | 225 |
else if (entry.entry_name.readable(db)) { |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
226 |
if (strict) { |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
227 |
val msg = message("Duplicate export", entry.theory_name, entry.name) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
228 |
errors.change(msg :: _) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
229 |
} |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
230 |
Exn.Res(()) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
231 |
} |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
232 |
else Exn.capture { entry.write(db) } |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
233 |
} |
70499 | 234 |
} |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
235 |
(results, true) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
236 |
}) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
237 |
|
77681
1db732e6c3d2
back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
wenzelm
parents:
77599
diff
changeset
|
238 |
def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = { |
75762
985c3a64748c
clarified signature: more uniform treatment of empty exports;
wenzelm
parents:
75759
diff
changeset
|
239 |
if (!progress.stopped && !body.is_empty) { |
76851 | 240 |
consumer.send(Entry.make(session_name, args, body, cache) -> args.strict) |
74257 | 241 |
} |
242 |
} |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
243 |
|
75393 | 244 |
def shutdown(close: Boolean = false): List[String] = { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
245 |
consumer.shutdown() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
246 |
if (close) db.close() |
74255 | 247 |
errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
248 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
249 |
} |
68116 | 250 |
|
251 |
||
75786 | 252 |
/* context for database access */ |
75772 | 253 |
|
75786 | 254 |
def open_database_context(store: Sessions.Store): Database_Context = { |
255 |
val database_server = if (store.database_server) Some(store.open_database_server()) else None |
|
256 |
new Database_Context(store, database_server) |
|
257 |
} |
|
258 |
||
259 |
def open_session_context0(store: Sessions.Store, session: String): Session_Context = |
|
260 |
open_database_context(store).open_session0(session, close_database_context = true) |
|
75772 | 261 |
|
75786 | 262 |
def open_session_context( |
263 |
store: Sessions.Store, |
|
76656 | 264 |
session_background: Sessions.Background, |
75786 | 265 |
document_snapshot: Option[Document.Snapshot] = None |
266 |
): Session_Context = { |
|
267 |
open_database_context(store).open_session( |
|
76656 | 268 |
session_background, document_snapshot = document_snapshot, close_database_context = true) |
75786 | 269 |
} |
75771 | 270 |
|
75786 | 271 |
class Database_Context private[Export]( |
272 |
val store: Sessions.Store, |
|
273 |
val database_server: Option[SQL.Database] |
|
274 |
) extends AutoCloseable { |
|
275 |
database_context => |
|
75782
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
276 |
|
75786 | 277 |
override def toString: String = { |
278 |
val s = |
|
279 |
database_server match { |
|
280 |
case Some(db) => db.toString |
|
281 |
case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ") |
|
282 |
} |
|
283 |
"Database_Context(" + s + ")" |
|
284 |
} |
|
285 |
||
286 |
def cache: Term.Cache = store.cache |
|
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
287 |
|
75786 | 288 |
def close(): Unit = database_server.foreach(_.close()) |
289 |
||
75970 | 290 |
def open_database(session: String, output: Boolean = false): Session_Database = |
75786 | 291 |
database_server match { |
75787 | 292 |
case Some(db) => new Session_Database(session, db) |
293 |
case None => |
|
75970 | 294 |
new Session_Database(session, store.open_database(session, output = output)) { |
75787 | 295 |
override def close(): Unit = db.close() |
296 |
} |
|
75786 | 297 |
} |
298 |
||
299 |
def open_session0(session: String, close_database_context: Boolean = false): Session_Context = |
|
76656 | 300 |
open_session(Sessions.background0(session), close_database_context = close_database_context) |
75779
5470c67bd772
clarified signature: prefer Export.Session_Context;
wenzelm
parents:
75778
diff
changeset
|
301 |
|
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
302 |
def open_session( |
76656 | 303 |
session_background: Sessions.Background, |
75772 | 304 |
document_snapshot: Option[Document.Snapshot] = None, |
75786 | 305 |
close_database_context: Boolean = false |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
306 |
): Session_Context = { |
76656 | 307 |
val session_name = session_background.check_errors.session_name |
308 |
val session_hierarchy = session_background.sessions_structure.build_hierarchy(session_name) |
|
75773
11b2bf6f90d8
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
wenzelm
parents:
75772
diff
changeset
|
309 |
val session_databases = |
75786 | 310 |
database_server match { |
75771 | 311 |
case Some(db) => session_hierarchy.map(name => new Session_Database(name, db)) |
312 |
case None => |
|
75775
70a65ee4a738
clarified signature: more robust treatment of server;
wenzelm
parents:
75774
diff
changeset
|
313 |
val attempts = |
70a65ee4a738
clarified signature: more robust treatment of server;
wenzelm
parents:
75774
diff
changeset
|
314 |
session_hierarchy.map(name => name -> store.try_open_database(name, server = false)) |
75771 | 315 |
attempts.collectFirst({ case (name, None) => name }) match { |
316 |
case Some(bad) => |
|
317 |
for ((_, Some(db)) <- attempts) db.close() |
|
75791 | 318 |
store.error_database(bad) |
75764
07e097f60b85
clarified signature: more robust close operation;
wenzelm
parents:
75762
diff
changeset
|
319 |
case None => |
75771 | 320 |
for ((name, Some(db)) <- attempts) yield { |
75764
07e097f60b85
clarified signature: more robust close operation;
wenzelm
parents:
75762
diff
changeset
|
321 |
new Session_Database(name, db) { override def close(): Unit = this.db.close() } |
07e097f60b85
clarified signature: more robust close operation;
wenzelm
parents:
75762
diff
changeset
|
322 |
} |
07e097f60b85
clarified signature: more robust close operation;
wenzelm
parents:
75762
diff
changeset
|
323 |
} |
75771 | 324 |
} |
76656 | 325 |
new Session_Context( |
326 |
database_context, session_background, session_databases, document_snapshot) { |
|
75772 | 327 |
override def close(): Unit = { |
328 |
session_databases.foreach(_.close()) |
|
75786 | 329 |
if (close_database_context) database_context.close() |
75772 | 330 |
} |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
331 |
} |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
332 |
} |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
333 |
} |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
334 |
|
75789 | 335 |
class Session_Database private[Export](val session: String, val db: SQL.Database) |
336 |
extends AutoCloseable { |
|
337 |
def close(): Unit = () |
|
338 |
||
339 |
lazy private [Export] val theory_names: List[String] = read_theory_names(db, session) |
|
340 |
lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session) |
|
341 |
} |
|
342 |
||
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
343 |
class Session_Context private[Export]( |
75786 | 344 |
val database_context: Database_Context, |
76656 | 345 |
session_background: Sessions.Background, |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
346 |
db_hierarchy: List[Session_Database], |
77005 | 347 |
val document_snapshot: Option[Document.Snapshot] |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
348 |
) extends AutoCloseable { |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
349 |
session_context => |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
350 |
|
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
351 |
def close(): Unit = () |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
352 |
|
75786 | 353 |
def cache: Term.Cache = database_context.cache |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
354 |
|
76656 | 355 |
def sessions_structure: Sessions.Structure = session_background.sessions_structure |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
356 |
|
76656 | 357 |
def session_base: Sessions.Base = session_background.base |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
358 |
|
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
359 |
def session_name: String = |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
360 |
if (document_snapshot.isDefined) Sessions.DRAFT |
75773
11b2bf6f90d8
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
wenzelm
parents:
75772
diff
changeset
|
361 |
else session_base.session_name |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
362 |
|
75780
f49c4f160b84
clarified signature: find session_database within Session_Context.db_hierarchy;
wenzelm
parents:
75779
diff
changeset
|
363 |
def session_database(session: String = session_name): Option[Session_Database] = |
f49c4f160b84
clarified signature: find session_database within Session_Context.db_hierarchy;
wenzelm
parents:
75779
diff
changeset
|
364 |
db_hierarchy.find(_.session == session) |
f49c4f160b84
clarified signature: find session_database within Session_Context.db_hierarchy;
wenzelm
parents:
75779
diff
changeset
|
365 |
|
f49c4f160b84
clarified signature: find session_database within Session_Context.db_hierarchy;
wenzelm
parents:
75779
diff
changeset
|
366 |
def session_db(session: String = session_name): Option[SQL.Database] = |
f49c4f160b84
clarified signature: find session_database within Session_Context.db_hierarchy;
wenzelm
parents:
75779
diff
changeset
|
367 |
session_database(session = session).map(_.db) |
f49c4f160b84
clarified signature: find session_database within Session_Context.db_hierarchy;
wenzelm
parents:
75779
diff
changeset
|
368 |
|
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
369 |
def session_stack: List[String] = |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
370 |
((if (document_snapshot.isDefined) List(session_name) else Nil) ::: |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
371 |
db_hierarchy.map(_.session)).reverse |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
372 |
|
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
373 |
private def select[A]( |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
374 |
session: String, |
75860
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
375 |
select: Session_Database => List[A], |
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
376 |
project: Entry_Name => A, |
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
377 |
sort_key: A => String |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
378 |
): List[A] = { |
75860
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
379 |
def result(name: String): List[A] = |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
380 |
if (name == Sessions.DRAFT) { |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
381 |
(for { |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
382 |
snapshot <- document_snapshot.iterator |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
383 |
entry_name <- snapshot.all_exports.keysIterator |
75860
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
384 |
} yield project(entry_name)).toSet.toList.sortBy(sort_key) |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
385 |
} |
75860
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
386 |
else session_database(name).map(select).getOrElse(Nil) |
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
387 |
|
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
388 |
if (session.nonEmpty) result(session) else session_stack.flatMap(result) |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
389 |
} |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
390 |
|
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
391 |
def entry_names(session: String = session_name): List[Entry_Name] = |
75860
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
392 |
select(session, _.entry_names, identity, _.compound_name) |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
393 |
|
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
394 |
def theory_names(session: String = session_name): List[String] = |
75860
2b2c09f4e7b5
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
wenzelm
parents:
75825
diff
changeset
|
395 |
select(session, _.theory_names, _.theory, identity) |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
396 |
|
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
397 |
def get(theory: String, name: String): Option[Entry] = |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
398 |
{ |
75784 | 399 |
def snapshot_entry: Option[Entry] = |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
400 |
for { |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
401 |
snapshot <- document_snapshot |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
402 |
entry_name = Entry_Name(session = Sessions.DRAFT, theory = theory, name = name) |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
403 |
entry <- snapshot.all_exports.get(entry_name) |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
404 |
} yield entry |
75784 | 405 |
def db_entry: Option[Entry] = |
406 |
db_hierarchy.view.map(database => |
|
407 |
Export.Entry_Name(session = database.session, theory = theory, name = name) |
|
408 |
.read(database.db, cache)) |
|
75764
07e097f60b85
clarified signature: more robust close operation;
wenzelm
parents:
75762
diff
changeset
|
409 |
.collectFirst({ case Some(entry) => entry }) |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
410 |
|
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
411 |
snapshot_entry orElse db_entry |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
412 |
} |
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
413 |
|
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
414 |
def apply(theory: String, name: String, permissive: Boolean = false): Entry = |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
415 |
get(theory, name) match { |
76851 | 416 |
case None if permissive => Entry.empty(theory, name) |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
417 |
case None => error("Missing export entry " + quote(compound_name(theory, name))) |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
418 |
case Some(entry) => entry |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
419 |
} |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
420 |
|
75790
0ab8a9177e41
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
wenzelm
parents:
75789
diff
changeset
|
421 |
def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context = |
0ab8a9177e41
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
wenzelm
parents:
75789
diff
changeset
|
422 |
new Theory_Context(session_context, theory, other_cache) |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
423 |
|
76910 | 424 |
def get_source_file(name: String): Option[Sessions.Source_File] = { |
76909 | 425 |
val store = database_context.store |
426 |
(for { |
|
427 |
database <- db_hierarchy.iterator |
|
428 |
file <- store.read_sources(database.db, database.session, name = name).iterator |
|
429 |
} yield file).nextOption() |
|
430 |
} |
|
431 |
||
76910 | 432 |
def source_file(name: String): Sessions.Source_File = |
433 |
get_source_file(name).getOrElse(error("Missing session source file " + quote(name))) |
|
434 |
||
77023
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
435 |
def theory_source(theory: String, unicode_symbols: Boolean = false): String = { |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
436 |
def snapshot_source: Option[String] = |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
437 |
for { |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
438 |
snapshot <- document_snapshot |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
439 |
text <- snapshot.version.nodes.iterator.collectFirst( |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
440 |
{ case (name, node) if name.theory == theory => node.source }) |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
441 |
if text.nonEmpty |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
442 |
} yield Symbol.output(unicode_symbols, text) |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
443 |
|
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
444 |
def db_source: Option[String] = { |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
445 |
val theory_context = session_context.theory(theory) |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
446 |
for { |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
447 |
name <- theory_context.files0(permissive = true).headOption |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
448 |
file <- get_source_file(name) |
77168
547d140f0780
more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant;
wenzelm
parents:
77026
diff
changeset
|
449 |
} yield Symbol.output(unicode_symbols, file.bytes.text) |
77023
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
450 |
} |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
451 |
|
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
452 |
snapshot_source orElse db_source getOrElse "" |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
453 |
} |
474a07221c27
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
wenzelm
parents:
77005
diff
changeset
|
454 |
|
75825 | 455 |
def classpath(): List[File.Content] = { |
75782
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
456 |
(for { |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
457 |
session <- session_stack.iterator |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
458 |
info <- sessions_structure.get(session).iterator |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
459 |
if info.export_classpath.nonEmpty |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
460 |
matcher = make_matcher(info.export_classpath) |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
461 |
entry_name <- entry_names(session = session).iterator |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
462 |
if matcher(entry_name) |
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
463 |
entry <- get(entry_name.theory, entry_name.name).iterator |
76852 | 464 |
} yield File.content(entry.entry_name.make_path(), entry.bytes)).toList |
75918 | 465 |
} |
75782
dba571dd0ba9
clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
wenzelm
parents:
75780
diff
changeset
|
466 |
|
75918 | 467 |
override def toString: String = |
75770
62e2c6f65f9a
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
wenzelm
parents:
75769
diff
changeset
|
468 |
"Export.Session_Context(" + commas_quote(session_stack) + ")" |
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
469 |
} |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
470 |
|
75774
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
471 |
class Theory_Context private[Export]( |
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
472 |
val session_context: Session_Context, |
75790
0ab8a9177e41
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
wenzelm
parents:
75789
diff
changeset
|
473 |
val theory: String, |
0ab8a9177e41
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
wenzelm
parents:
75789
diff
changeset
|
474 |
other_cache: Option[Term.Cache] |
75774
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
475 |
) { |
75790
0ab8a9177e41
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
wenzelm
parents:
75789
diff
changeset
|
476 |
def cache: Term.Cache = other_cache getOrElse session_context.cache |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
477 |
|
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
478 |
def get(name: String): Option[Entry] = session_context.get(theory, name) |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
479 |
def apply(name: String, permissive: Boolean = false): Entry = |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
480 |
session_context.apply(theory, name, permissive = permissive) |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
481 |
|
76854 | 482 |
def yxml(name: String): XML.Body = |
75774
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
483 |
get(name) match { |
76852 | 484 |
case Some(entry) => entry.yxml |
75774
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
485 |
case None => Nil |
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
486 |
} |
efc25bf4b795
discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents:
75773
diff
changeset
|
487 |
|
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
488 |
def document_id(): Option[Long] = |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
489 |
apply(DOCUMENT_ID, permissive = true).text match { |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
490 |
case Value.Long(id) => Some(id) |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
491 |
case _ => None |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
492 |
} |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
493 |
|
75901 | 494 |
def files0(permissive: Boolean = false): List[String] = |
495 |
split_lines(apply(FILES, permissive = permissive).text) |
|
496 |
||
497 |
def files(permissive: Boolean = false): Option[(String, List[String])] = |
|
498 |
files0(permissive = permissive) match { |
|
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
499 |
case Nil => None |
75901 | 500 |
case a :: bs => Some((a, bs)) |
75778
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
501 |
} |
d18c96b9b955
prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents:
75775
diff
changeset
|
502 |
|
75759
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
503 |
override def toString: String = "Export.Theory_Context(" + quote(theory) + ")" |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
504 |
} |
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
505 |
|
0cdccd0d1699
clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents:
75757
diff
changeset
|
506 |
|
68288 | 507 |
/* export to file-system */ |
508 |
||
509 |
def export_files( |
|
510 |
store: Sessions.Store, |
|
511 |
session_name: String, |
|
512 |
export_dir: Path, |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71624
diff
changeset
|
513 |
progress: Progress = new Progress, |
69671 | 514 |
export_prune: Int = 0, |
68288 | 515 |
export_list: Boolean = false, |
75393 | 516 |
export_patterns: List[String] = Nil |
517 |
): Unit = { |
|
75394 | 518 |
using(store.open_database(session_name)) { db => |
75739
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
519 |
val entry_names = read_entry_names(db, session_name) |
68288 | 520 |
|
75739
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
521 |
// list |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
522 |
if (export_list) { |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
523 |
for (entry_name <- entry_names) progress.echo(entry_name.compound_name) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
524 |
} |
68288 | 525 |
|
75739
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
526 |
// export |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
527 |
if (export_patterns.nonEmpty) { |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
528 |
val matcher = make_matcher(export_patterns) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
529 |
for { |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
530 |
entry_name <- entry_names if matcher(entry_name) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
531 |
entry <- entry_name.read(db, store.cache) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
532 |
} { |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
533 |
val path = export_dir + entry_name.make_path(prune = export_prune) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
534 |
progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
535 |
Isabelle_System.make_directory(path.dir) |
76852 | 536 |
val bytes = entry.bytes |
75739
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
537 |
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes) |
5b37466c1463
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents:
75736
diff
changeset
|
538 |
File.set_executable(path, entry.executable) |
68288 | 539 |
} |
540 |
} |
|
75394 | 541 |
} |
68288 | 542 |
} |
543 |
||
544 |
||
68116 | 545 |
/* Isabelle tool wrapper */ |
546 |
||
71601 | 547 |
val default_export_dir: Path = Path.explode("export") |
68116 | 548 |
|
75394 | 549 |
val isabelle_tool = |
550 |
Isabelle_Tool("export", "retrieve theory exports", Scala_Project.here, |
|
551 |
{ args => |
|
552 |
/* arguments */ |
|
68116 | 553 |
|
75394 | 554 |
var export_dir = default_export_dir |
555 |
var dirs: List[Path] = Nil |
|
556 |
var export_list = false |
|
557 |
var no_build = false |
|
558 |
var options = Options.init() |
|
559 |
var export_prune = 0 |
|
560 |
var export_patterns: List[String] = Nil |
|
68116 | 561 |
|
75394 | 562 |
val getopts = Getopts(""" |
68116 | 563 |
Usage: isabelle export [OPTIONS] SESSION |
564 |
||
565 |
Options are: |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68305
diff
changeset
|
566 |
-O DIR output directory for exported files (default: """ + default_export_dir + """) |
68116 | 567 |
-d DIR include session directory |
568 |
-l list exports |
|
569 |
-n no build of session |
|
570 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
69671 | 571 |
-p NUM prune path of exported files by NUM elements |
68116 | 572 |
-x PATTERN extract files matching pattern (e.g. "*:**" for all) |
573 |
||
574 |
List or export theory exports for SESSION: named blobs produced by |
|
68290 | 575 |
isabelle build. Option -l or -x is required; option -x may be repeated. |
68116 | 576 |
|
577 |
The PATTERN language resembles glob patterns in the shell, with ? and * |
|
578 |
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], |
|
579 |
and variants {pattern1,pattern2,pattern3}. |
|
580 |
""", |
|
75394 | 581 |
"O:" -> (arg => export_dir = Path.explode(arg)), |
582 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
583 |
"l" -> (_ => export_list = true), |
|
584 |
"n" -> (_ => no_build = true), |
|
585 |
"o:" -> (arg => options = options + arg), |
|
586 |
"p:" -> (arg => export_prune = Value.Int.parse(arg)), |
|
587 |
"x:" -> (arg => export_patterns ::= arg)) |
|
68116 | 588 |
|
75394 | 589 |
val more_args = getopts(args) |
590 |
val session_name = |
|
591 |
more_args match { |
|
592 |
case List(session_name) if export_list || export_patterns.nonEmpty => session_name |
|
593 |
case _ => getopts.usage() |
|
594 |
} |
|
68116 | 595 |
|
75394 | 596 |
val progress = new Console_Progress() |
68305 | 597 |
|
68116 | 598 |
|
75394 | 599 |
/* build */ |
68116 | 600 |
|
75394 | 601 |
if (!no_build) { |
602 |
val rc = |
|
603 |
progress.interrupt_handler { |
|
604 |
Build.build_logic(options, session_name, progress = progress, dirs = dirs) |
|
605 |
} |
|
606 |
if (rc != Process_Result.RC.ok) sys.exit(rc) |
|
68331 | 607 |
} |
68116 | 608 |
|
609 |
||
75394 | 610 |
/* export files */ |
68116 | 611 |
|
75394 | 612 |
val store = Sessions.store(options) |
613 |
export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, |
|
614 |
export_list = export_list, export_patterns = export_patterns) |
|
615 |
}) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
616 |
} |