--- a/src/Pure/Thy/export_theory.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala Fri May 18 17:09:55 2018 +0200
@@ -23,13 +23,11 @@
theory_graph.topological_order.map(theory_graph.get_node(_))
}
- def read_session(session_name: String,
- system_mode: Boolean = false,
+ def read_session(store: Sessions.Store,
+ session_name: String,
types: Boolean = true,
consts: Boolean = true): Session =
{
- val store = Sessions.store(system_mode)
-
val thys =
using(SQLite.open_database(store.the_database(session_name)))(db =>
{