251 def shutdown(close: Boolean = false): List[String] = { |
251 def shutdown(close: Boolean = false): List[String] = { |
252 consumer.shutdown() |
252 consumer.shutdown() |
253 if (close) db.close() |
253 if (close) db.close() |
254 errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil) |
254 errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil) |
255 } |
255 } |
256 } |
|
257 |
|
258 |
|
259 /* abstract provider */ |
|
260 |
|
261 object Provider { |
|
262 private def database_provider( |
|
263 db: SQL.Database, |
|
264 cache: XML.Cache, |
|
265 session: String, |
|
266 theory: String, |
|
267 _theory_names: Synchronized[Option[List[String]]] |
|
268 ): Provider = { |
|
269 new Provider { |
|
270 override def theory_names: List[String] = |
|
271 _theory_names.change_result { st => |
|
272 val res = st.getOrElse(read_theory_names(db, session)) |
|
273 (res, Some(res)) |
|
274 } |
|
275 |
|
276 override def apply(export_name: String): Option[Entry] = |
|
277 if (theory.isEmpty) None |
|
278 else { |
|
279 Entry_Name(session = session, theory = theory, name = export_name) |
|
280 .read(db, cache) |
|
281 } |
|
282 |
|
283 override def focus(other_theory: String): Provider = |
|
284 if (other_theory == theory) this |
|
285 else database_provider(db, cache, session, theory, _theory_names) |
|
286 |
|
287 override def toString: String = db.toString |
|
288 } |
|
289 } |
|
290 |
|
291 def database( |
|
292 db: SQL.Database, |
|
293 cache: XML.Cache, |
|
294 session: String, |
|
295 theory: String = "" |
|
296 ): Provider = database_provider(db, cache, session, theory, Synchronized(None)) |
|
297 |
|
298 def snapshot( |
|
299 resources: Resources, |
|
300 snapshot: Document.Snapshot |
|
301 ): Provider = |
|
302 new Provider { |
|
303 override def theory_names: List[String] = |
|
304 (for { |
|
305 (name, _) <- snapshot.version.nodes.iterator |
|
306 if name.is_theory && !resources.session_base.loaded_theory(name) |
|
307 } yield name.theory).toList |
|
308 |
|
309 override def apply(name: String): Option[Entry] = |
|
310 snapshot.all_exports.get( |
|
311 Entry_Name(session = Sessions.DRAFT, theory = snapshot.node_name.theory, name = name)) |
|
312 |
|
313 override def focus(other_theory: String): Provider = |
|
314 if (other_theory == snapshot.node_name.theory) this |
|
315 else { |
|
316 val node_name = |
|
317 snapshot.version.nodes.theory_name(other_theory) getOrElse |
|
318 error("Bad theory " + quote(other_theory)) |
|
319 Provider.snapshot(resources, snapshot.state.snapshot(node_name)) |
|
320 } |
|
321 |
|
322 override def toString: String = snapshot.toString |
|
323 } |
|
324 } |
|
325 |
|
326 trait Provider { |
|
327 def theory_names: List[String] |
|
328 |
|
329 def apply(export_name: String): Option[Entry] |
|
330 |
|
331 def uncompressed_yxml(export_name: String): XML.Body = |
|
332 apply(export_name) match { |
|
333 case Some(entry) => entry.uncompressed_yxml |
|
334 case None => Nil |
|
335 } |
|
336 |
|
337 def focus(other_theory: String): Provider |
|
338 } |
256 } |
339 |
257 |
340 |
258 |
341 /* context for retrieval */ |
259 /* context for retrieval */ |
342 |
260 |
471 |
389 |
472 override def toString: String = |
390 override def toString: String = |
473 "Export.Session_Context(" + commas_quote(session_stack) + ")" |
391 "Export.Session_Context(" + commas_quote(session_stack) + ")" |
474 } |
392 } |
475 |
393 |
476 class Theory_Context private[Export](val session_context: Session_Context, theory: String) { |
394 class Theory_Context private[Export]( |
|
395 val session_context: Session_Context, |
|
396 val theory: String |
|
397 ) { |
477 def get(name: String): Option[Entry] = session_context.get(theory, name) |
398 def get(name: String): Option[Entry] = session_context.get(theory, name) |
478 def apply(name: String, permissive: Boolean = false): Entry = |
399 def apply(name: String, permissive: Boolean = false): Entry = |
479 session_context.apply(theory, name, permissive = permissive) |
400 session_context.apply(theory, name, permissive = permissive) |
|
401 |
|
402 def uncompressed_yxml(name: String): XML.Body = |
|
403 get(name) match { |
|
404 case Some(entry) => entry.uncompressed_yxml |
|
405 case None => Nil |
|
406 } |
480 |
407 |
481 override def toString: String = "Export.Theory_Context(" + quote(theory) + ")" |
408 override def toString: String = "Export.Theory_Context(" + quote(theory) + ")" |
482 } |
409 } |
483 |
410 |
484 |
411 |