renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
--- a/src/Pure/ML/ml_heap.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala Tue Jul 18 19:51:12 2023 +0200
@@ -43,7 +43,7 @@
/* SQL data model */
- object Data extends SQL.Data("isabelle_heaps") {
+ object private_data extends SQL.Data("isabelle_heaps") {
override lazy val tables = SQL.Tables(Base.table, Slices.table)
object Generic {
@@ -123,13 +123,13 @@
}
def clean_entry(db: SQL.Database, session_name: String): Unit =
- Data.transaction_lock(db, create = true, label = "ML_Heap.clean_entry") {
- Data.clean_entry(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "ML_Heap.clean_entry") {
+ private_data.clean_entry(db, session_name)
}
def get_entry(db: SQL.Database, session_name: String): Option[SHA1.Digest] =
- Data.transaction_lock(db, create = true, label = "ML_Heap.get_entry") {
- Data.get_entry(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "ML_Heap.get_entry") {
+ private_data.get_entry(db, session_name)
}
def store(
@@ -149,8 +149,8 @@
val step = (size.toDouble / slices.toDouble).ceil.toLong
try {
- Data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
- Data.prepare_entry(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
+ private_data.prepare_entry(db, session_name)
}
for (i <- 0 until slices) {
@@ -160,18 +160,18 @@
val content =
Bytes.read_file(heap.file, offset = offset, limit = limit)
.compress(cache = cache)
- Data.transaction_lock(db, label = "ML_Heap.store2") {
- Data.write_entry(db, session_name, i, content)
+ private_data.transaction_lock(db, label = "ML_Heap.store2") {
+ private_data.write_entry(db, session_name, i, content)
}
}
- Data.transaction_lock(db, label = "ML_Heap.store3") {
- Data.finish_entry(db, session_name, size, digest)
+ private_data.transaction_lock(db, label = "ML_Heap.store3") {
+ private_data.finish_entry(db, session_name, size, digest)
}
}
catch { case exn: Throwable =>
- Data.transaction_lock(db, create = true, label = "ML_Heap.store4") {
- Data.clean_entry(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "ML_Heap.store4") {
+ private_data.clean_entry(db, session_name)
}
throw exn
}
@@ -188,14 +188,14 @@
database match {
case None =>
case Some(db) =>
- Data.transaction_lock(db, create = true, label = "ML_Heap.restore") {
- val db_digest = Data.get_entry(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "ML_Heap.restore") {
+ val db_digest = private_data.get_entry(db, session_name)
val file_digest = read_file_digest(heap)
if (db_digest.isDefined && db_digest != file_digest) {
Isabelle_System.make_directory(heap.expand.dir)
Bytes.write(heap, Bytes.empty)
- for (slice <- Data.read_entry(db, session_name)) {
+ for (slice <- private_data.read_entry(db, session_name)) {
Bytes.append(heap, slice.uncompress(cache = cache))
}
val digest = write_file_digest(heap)
--- a/src/Pure/System/host.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/System/host.scala Tue Jul 18 19:51:12 2023 +0200
@@ -95,7 +95,7 @@
/* SQL data model */
- object Data extends SQL.Data("isabelle_host") {
+ object private_data extends SQL.Data("isabelle_host") {
val database: Path = Path.explode("$ISABELLE_HOME_USER/host.db")
override lazy val tables = SQL.Tables(Node_Info.table)
@@ -134,8 +134,8 @@
else {
val available = available_nodes.zipWithIndex
val used = used_nodes
- Data.transaction_lock(db, create = true, label = "Host.next_numa_node") {
- val numa_next = Data.read_numa_next(db, hostname)
+ private_data.transaction_lock(db, create = true, label = "Host.next_numa_node") {
+ val numa_next = private_data.read_numa_next(db, hostname)
val numa_index = available.collectFirst({ case (n, i) if n == numa_next => i }).getOrElse(0)
val candidates = available.drop(numa_index) ::: available.take(numa_index)
val (n, i) =
@@ -143,7 +143,7 @@
candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
val numa_next1 = available_nodes((i + 1) % available_nodes.length)
- if (numa_next != numa_next1) Data.write_numa_next(db, hostname, numa_next1)
+ if (numa_next != numa_next1) private_data.write_numa_next(db, hostname, numa_next1)
Some(n)
}
--- a/src/Pure/System/progress.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/System/progress.scala Tue Jul 18 19:51:12 2023 +0200
@@ -41,7 +41,7 @@
/* SQL data model */
- object Data extends SQL.Data("isabelle_progress") {
+ object private_data extends SQL.Data("isabelle_progress") {
val database: Path = Path.explode("$ISABELLE_HOME_USER/progress.db")
override lazy val tables = SQL.Tables(Base.table, Agents.table, Messages.table)
@@ -259,21 +259,21 @@
def agent_uuid: String = synchronized { _agent_uuid }
private def init(): Unit = synchronized {
- Progress.Data.transaction_lock(db, create = true, label = "Database_Progress.init") {
- Progress.Data.read_progress_context(db, context_uuid) match {
+ Progress.private_data.transaction_lock(db, create = true, label = "Database_Progress.init") {
+ Progress.private_data.read_progress_context(db, context_uuid) match {
case Some(context) =>
_context = context
_agent_uuid = UUID.random().toString
case None =>
- _context = Progress.Data.next_progress_context(db)
+ _context = Progress.private_data.next_progress_context(db)
_agent_uuid = context_uuid
- db.execute_statement(Progress.Data.Base.table.insert(), { stmt =>
+ db.execute_statement(Progress.private_data.Base.table.insert(), { stmt =>
stmt.string(1) = context_uuid
stmt.long(2) = _context
stmt.bool(3) = false
})
}
- db.execute_statement(Progress.Data.Agents.table.insert(), { stmt =>
+ db.execute_statement(Progress.private_data.Agents.table.insert(), { stmt =>
val java = ProcessHandle.current()
val java_pid = java.pid
val java_start = Date.instant(java.info.startInstant.get)
@@ -291,13 +291,13 @@
stmt.long(10) = 0L
})
}
- if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables.list)
+ if (context_uuid == _agent_uuid) db.vacuum(Progress.private_data.tables.list)
}
def exit(close: Boolean = false): Unit = synchronized {
if (_context > 0) {
- Progress.Data.transaction_lock(db, label = "Database_Progress.exit") {
- Progress.Data.update_agent(db, _agent_uuid, _seen, stop_now = true)
+ Progress.private_data.transaction_lock(db, label = "Database_Progress.exit") {
+ Progress.private_data.update_agent(db, _agent_uuid, _seen, stop_now = true)
}
_context = 0
}
@@ -308,19 +308,19 @@
if (_context < 0) throw new IllegalStateException("Database_Progress before init")
if (_context == 0) throw new IllegalStateException("Database_Progress after exit")
- Progress.Data.transaction_lock(db, label = "Database_Progress.sync") {
- val stopped_db = Progress.Data.read_progress_stopped(db, _context)
+ Progress.private_data.transaction_lock(db, label = "Database_Progress.sync") {
+ val stopped_db = Progress.private_data.read_progress_stopped(db, _context)
val stopped = base_progress.stopped
if (stopped_db && !stopped) base_progress.stop()
- if (stopped && !stopped_db) Progress.Data.write_progress_stopped(db, _context, true)
+ if (stopped && !stopped_db) Progress.private_data.write_progress_stopped(db, _context, true)
- val messages = Progress.Data.read_messages(db, _context, seen = _seen)
+ val messages = Progress.private_data.read_messages(db, _context, seen = _seen)
for ((seen, message) <- messages) {
if (base_progress.do_output(message)) base_progress.output(message)
_seen = _seen max seen
}
- if (messages.nonEmpty) Progress.Data.update_agent(db, _agent_uuid, _seen)
+ if (messages.nonEmpty) Progress.private_data.update_agent(db, _agent_uuid, _seen)
body
}
@@ -330,13 +330,13 @@
private def output_database(message: Progress.Message, body: => Unit): Unit =
sync_database {
- val serial = Progress.Data.next_messages_serial(db, _context)
- Progress.Data.write_messages(db, _context, serial, message)
+ val serial = Progress.private_data.next_messages_serial(db, _context)
+ Progress.private_data.write_messages(db, _context, serial, message)
body
_seen = _seen max serial
- Progress.Data.update_agent(db, _agent_uuid, _seen)
+ Progress.private_data.update_agent(db, _agent_uuid, _seen)
}
override def output(message: Progress.Message): Unit =
--- a/src/Pure/Thy/document_build.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/Thy/document_build.scala Tue Jul 18 19:51:12 2023 +0200
@@ -54,7 +54,7 @@
/* SQL data model */
- object Data extends SQL.Data("isabelle_documents") {
+ object private_data extends SQL.Data("isabelle_documents") {
override lazy val tables = SQL.Tables(Base.table)
object Base {
@@ -104,18 +104,18 @@
}
def clean_session(db: SQL.Database, session_name: String): Unit =
- Data.transaction_lock(db, create = true, label = "Document_Build.clean_session") {
- Data.clean_session(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "Document_Build.clean_session") {
+ private_data.clean_session(db, session_name)
}
def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
- Data.transaction_lock(db, label = "Document_Build.read_document") {
- Data.read_document(db, session_name, name)
+ private_data.transaction_lock(db, label = "Document_Build.read_document") {
+ private_data.read_document(db, session_name, name)
}
def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
- Data.transaction_lock(db, label = "Document_Build.write_document") {
- Data.write_document(db, session_name, doc)
+ private_data.transaction_lock(db, label = "Document_Build.write_document") {
+ private_data.write_document(db, session_name, doc)
}
--- a/src/Pure/Thy/export.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/Thy/export.scala Tue Jul 18 19:51:12 2023 +0200
@@ -29,7 +29,7 @@
/* SQL data model */
- object Data extends SQL.Data() {
+ object private_data extends SQL.Data() {
override lazy val tables = SQL.Tables(Base.table)
object Base {
@@ -63,7 +63,7 @@
def read_entry(db: SQL.Database, entry_name: Entry_Name, cache: XML.Cache): Option[Entry] =
db.execute_query_statementO[Entry](
Base.table.select(List(Base.executable, Base.compressed, Base.body),
- sql = Data.where_equal(entry_name.session, entry_name.theory, entry_name.name)),
+ sql = private_data.where_equal(entry_name.session, entry_name.theory, entry_name.name)),
{ res =>
val executable = res.bool(Base.executable)
val compressed = res.bool(Base.compressed)
@@ -88,13 +88,13 @@
def read_theory_names(db: SQL.Database, session_name: String): List[String] =
db.execute_query_statement(
Base.table.select(List(Base.theory_name), distinct = true,
- sql = Data.where_equal(session_name) + SQL.order_by(List(Base.theory_name))),
+ sql = private_data.where_equal(session_name) + SQL.order_by(List(Base.theory_name))),
List.from[String], res => res.string(Base.theory_name))
def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] =
db.execute_query_statement(
Base.table.select(List(Base.theory_name, Base.name),
- sql = Data.where_equal(session_name)) + SQL.order_by(List(Base.theory_name, Base.name)),
+ sql = private_data.where_equal(session_name)) + SQL.order_by(List(Base.theory_name, Base.name)),
List.from[Entry_Name],
{ res =>
Entry_Name(
@@ -204,23 +204,23 @@
}
def clean_session(db: SQL.Database, session_name: String): Unit =
- Data.transaction_lock(db, create = true, label = "Export.clean_session") {
- Data.clean_session(db, session_name)
+ private_data.transaction_lock(db, create = true, label = "Export.clean_session") {
+ private_data.clean_session(db, session_name)
}
def read_theory_names(db: SQL.Database, session_name: String): List[String] =
- Data.transaction_lock(db, label = "Export.read_theory_names") {
- Data.read_theory_names(db, session_name)
+ private_data.transaction_lock(db, label = "Export.read_theory_names") {
+ private_data.read_theory_names(db, session_name)
}
def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] =
- Data.transaction_lock(db, label = "Export.read_entry_names") {
- Data.read_entry_names(db, session_name)
+ private_data.transaction_lock(db, label = "Export.read_entry_names") {
+ private_data.read_entry_names(db, session_name)
}
def read_entry(db: SQL.Database, entry_name: Entry_Name, cache: XML.Cache): Option[Entry] =
- Data.transaction_lock(db, label = "Export.read_entry") {
- Data.read_entry(db, entry_name, cache)
+ private_data.transaction_lock(db, label = "Export.read_entry") {
+ private_data.read_entry(db, entry_name, cache)
}
@@ -238,21 +238,21 @@
consume =
{ (args: List[(Entry, Boolean)]) =>
val results =
- Data.transaction_lock(db, label = "Export.consumer(" + args.length + ")") {
+ private_data.transaction_lock(db, label = "Export.consumer(" + args.length + ")") {
for ((entry, strict) <- args)
yield {
if (progress.stopped) {
entry.cancel()
Exn.Res(())
}
- else if (Data.readable_entry(db, entry.entry_name)) {
+ else if (private_data.readable_entry(db, entry.entry_name)) {
if (strict) {
val msg = message("Duplicate export", entry.theory_name, entry.name)
errors.change(msg :: _)
}
Exn.Res(())
}
- else Exn.capture { Data.write_entry(db, entry) }
+ else Exn.capture { private_data.write_entry(db, entry) }
}
}
(results, true)
--- a/src/Pure/Thy/store.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/Thy/store.scala Tue Jul 18 19:51:12 2023 +0200
@@ -77,7 +77,7 @@
/* SQL data model */
- object Data extends SQL.Data() {
+ object private_data extends SQL.Data() {
override lazy val tables = SQL.Tables(Session_Info.table, Sources.table)
object Session_Info {
@@ -417,26 +417,26 @@
/* session info */
def session_info_exists(db: SQL.Database): Boolean =
- Store.Data.tables.forall(db.exists_table)
+ Store.private_data.tables.forall(db.exists_table)
def session_info_defined(db: SQL.Database, name: String): Boolean =
db.execute_query_statementB(
- Store.Data.Session_Info.table.select(List(Store.Data.Session_Info.session_name),
- sql = Store.Data.Session_Info.session_name.where_equal(name)))
+ Store.private_data.Session_Info.table.select(List(Store.private_data.Session_Info.session_name),
+ sql = Store.private_data.Session_Info.session_name.where_equal(name)))
def clean_session_info(db: SQL.Database, name: String): Boolean = {
Export.clean_session(db, name)
Document_Build.clean_session(db, name)
- Store.Data.transaction_lock(db, create = true, label = "Store.clean_session_info") {
+ Store.private_data.transaction_lock(db, create = true, label = "Store.clean_session_info") {
val already_defined = session_info_defined(db, name)
db.execute_statement(
- Store.Data.Session_Info.table.delete(
- sql = Store.Data.Session_Info.session_name.where_equal(name)))
+ Store.private_data.Session_Info.table.delete(
+ sql = Store.private_data.Session_Info.session_name.where_equal(name)))
- db.execute_statement(Store.Data.Sources.table.delete(
- sql = Store.Data.Sources.where_equal(name)))
+ db.execute_statement(Store.private_data.Sources.table.delete(
+ sql = Store.private_data.Sources.where_equal(name)))
already_defined
}
@@ -449,52 +449,52 @@
build_log: Build_Log.Session_Info,
build: Store.Build_Info
): Unit = {
- Store.Data.transaction_lock(db, label = "Store.write_session_info") {
- Store.Data.write_sources(db, session_name, sources)
- Store.Data.write_session_info(db, cache.compress, session_name, build_log, build)
+ Store.private_data.transaction_lock(db, label = "Store.write_session_info") {
+ Store.private_data.write_sources(db, session_name, sources)
+ Store.private_data.write_session_info(db, cache.compress, session_name, build_log, build)
}
}
def read_session_timing(db: SQL.Database, session: String): Properties.T =
- Store.Data.transaction_lock(db, label = "Store.read_session_timing") {
- Store.Data.read_session_timing(db, session, cache)
+ Store.private_data.transaction_lock(db, label = "Store.read_session_timing") {
+ Store.private_data.read_session_timing(db, session, cache)
}
def read_command_timings(db: SQL.Database, session: String): Bytes =
- Store.Data.transaction_lock(db, label = "Store.read_command_timings") {
- Store.Data.read_command_timings(db, session)
+ Store.private_data.transaction_lock(db, label = "Store.read_command_timings") {
+ Store.private_data.read_command_timings(db, session)
}
def read_theory_timings(db: SQL.Database, session: String): List[Properties.T] =
- Store.Data.transaction_lock(db, label = "Store.read_theory_timings") {
- Store.Data.read_theory_timings(db, session, cache)
+ Store.private_data.transaction_lock(db, label = "Store.read_theory_timings") {
+ Store.private_data.read_theory_timings(db, session, cache)
}
def read_ml_statistics(db: SQL.Database, session: String): List[Properties.T] =
- Store.Data.transaction_lock(db, label = "Store.read_ml_statistics") {
- Store.Data.read_ml_statistics(db, session, cache)
+ Store.private_data.transaction_lock(db, label = "Store.read_ml_statistics") {
+ Store.private_data.read_ml_statistics(db, session, cache)
}
def read_task_statistics(db: SQL.Database, session: String): List[Properties.T] =
- Store.Data.transaction_lock(db, label = "Store.read_task_statistics") {
- Store.Data.read_task_statistics(db, session, cache)
+ Store.private_data.transaction_lock(db, label = "Store.read_task_statistics") {
+ Store.private_data.read_task_statistics(db, session, cache)
}
def read_theories(db: SQL.Database, session: String): List[String] =
read_theory_timings(db, session).flatMap(Markup.Name.unapply)
def read_errors(db: SQL.Database, session: String): List[String] =
- Store.Data.transaction_lock(db, label = "Store.read_errors") {
- Store.Data.read_errors(db, session, cache)
+ Store.private_data.transaction_lock(db, label = "Store.read_errors") {
+ Store.private_data.read_errors(db, session, cache)
}
def read_build(db: SQL.Database, session: String): Option[Store.Build_Info] =
- Store.Data.transaction_lock(db, label = "Store.read_build") {
- if (session_info_exists(db)) Store.Data.read_build(db, session) else None
+ Store.private_data.transaction_lock(db, label = "Store.read_build") {
+ if (session_info_exists(db)) Store.private_data.read_build(db, session) else None
}
def read_sources(db: SQL.Database, session: String, name: String = ""): List[Store.Source_File] =
- Store.Data.transaction_lock(db, label = "Store.read_sources") {
- Store.Data.read_sources(db, session, name, cache.compress)
+ Store.private_data.transaction_lock(db, label = "Store.read_sources") {
+ Store.private_data.read_sources(db, session, name, cache.compress)
}
}
--- a/src/Pure/Tools/build_process.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Tue Jul 18 19:51:12 2023 +0200
@@ -283,7 +283,7 @@
/** SQL data model **/
- object Data extends SQL.Data("isabelle_build") {
+ object private_data extends SQL.Data("isabelle_build") {
val database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
def pull[A <: Library.Named](
@@ -364,7 +364,7 @@
})
for (build <- builds.sortBy(_.start)(Date.Ordering)) yield {
- val sessions = Data.read_sessions_domain(db, build_uuid = build.build_uuid)
+ val sessions = private_data.read_sessions_domain(db, build_uuid = build.build_uuid)
build.copy(sessions = sessions.toList.sorted)
}
}
@@ -828,8 +828,8 @@
}
def read_builds(db: SQL.Database): List[Build] =
- Data.transaction_lock(db, create = true, label = "Build_Process.read_builds") {
- Data.read_builds(db)
+ private_data.transaction_lock(db, create = true, label = "Build_Process.read_builds") {
+ private_data.read_builds(db)
}
}
@@ -862,16 +862,16 @@
try {
for (db <- store.maybe_open_build_database(server = server)) yield {
val store_tables = db.is_postgresql
- Build_Process.Data.transaction_lock(db,
+ Build_Process.private_data.transaction_lock(db,
create = true,
label = "Build_Process.build_database"
) {
- Build_Process.Data.clean_build(db)
- if (store_tables) Store.Data.tables.lock(db, create = true)
+ Build_Process.private_data.clean_build(db)
+ if (store_tables) Store.private_data.tables.lock(db, create = true)
}
if (build_context.master) {
- db.vacuum(Build_Process.Data.tables.list)
- if (store_tables) db.vacuum(Store.Data.tables.list)
+ db.vacuum(Build_Process.private_data.tables.list)
+ if (store_tables) db.vacuum(Store.private_data.tables.list)
}
db
}
@@ -879,7 +879,7 @@
catch { case exn: Throwable => close(); throw exn }
private val _host_database: Option[SQL.Database] =
- try { store.maybe_open_build_database(path = Host.Data.database, server = server) }
+ try { store.maybe_open_build_database(path = Host.private_data.database, server = server) }
catch { case exn: Throwable => close(); throw exn }
protected val (progress, worker_uuid) = synchronized {
@@ -887,7 +887,7 @@
case None => (build_progress, UUID.random().toString)
case Some(db) =>
try {
- val progress_db = store.open_build_database(Progress.Data.database, server = server)
+ val progress_db = store.open_build_database(Progress.private_data.database, server = server)
val progress =
new Database_Progress(progress_db, build_progress,
hostname = hostname,
@@ -922,11 +922,11 @@
case None => body
case Some(db) =>
progress.asInstanceOf[Database_Progress].sync()
- Build_Process.Data.transaction_lock(db, label = label) {
- _state = Build_Process.Data.pull_database(db, worker_uuid, hostname, _state)
+ Build_Process.private_data.transaction_lock(db, label = label) {
+ _state = Build_Process.private_data.pull_database(db, worker_uuid, hostname, _state)
val res = body
_state =
- Build_Process.Data.update_database(db, worker_uuid, build_uuid, hostname, _state)
+ Build_Process.private_data.update_database(db, worker_uuid, build_uuid, hostname, _state)
res
}
}
@@ -1046,27 +1046,27 @@
protected final def start_build(): Unit = synchronized_database("Build_Process.start_build") {
for (db <- _build_database) {
- Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
+ Build_Process.private_data.start_build(db, build_uuid, build_context.ml_platform,
build_context.sessions_structure.session_prefs)
}
}
protected final def stop_build(): Unit = synchronized_database("Build_Process.stop_build") {
for (db <- _build_database) {
- Build_Process.Data.stop_build(db, build_uuid)
+ Build_Process.private_data.stop_build(db, build_uuid)
}
}
protected final def start_worker(): Unit = synchronized_database("Build_Process.start_worker") {
for (db <- _build_database) {
_state = _state.inc_serial
- Build_Process.Data.start_worker(db, worker_uuid, build_uuid, _state.serial)
+ Build_Process.private_data.start_worker(db, worker_uuid, build_uuid, _state.serial)
}
}
protected final def stop_worker(): Unit = synchronized_database("Build_Process.stop_worker") {
for (db <- _build_database) {
- Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop_now = true)
+ Build_Process.private_data.stamp_worker(db, worker_uuid, _state.serial, stop_now = true)
}
}
@@ -1145,8 +1145,8 @@
_build_database match {
case None => (Nil, Nil)
case Some(db) =>
- (Build_Process.Data.read_builds(db),
- Build_Process.Data.read_workers(db))
+ (Build_Process.private_data.read_builds(db),
+ Build_Process.private_data.read_workers(db))
}
Build_Process.Snapshot(
builds = builds,
--- a/src/Pure/Tools/server.scala Tue Jul 18 13:34:18 2023 +0200
+++ b/src/Pure/Tools/server.scala Tue Jul 18 19:51:12 2023 +0200
@@ -363,7 +363,7 @@
val default_name = "isabelle"
- object Data extends SQL.Data() {
+ object private_data extends SQL.Data() {
val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
val name = SQL.Column.string("name").make_primary_key
@@ -375,13 +375,13 @@
}
def list(db: SQLite.Database): List[Info] =
- if (db.exists_table(Data.table)) {
- db.execute_query_statement(Data.table.select(),
+ if (db.exists_table(private_data.table)) {
+ db.execute_query_statement(private_data.table.select(),
List.from[Info],
{ res =>
- val name = res.string(Data.name)
- val port = res.int(Data.port)
- val password = res.string(Data.password)
+ val name = res.string(private_data.name)
+ val port = res.int(private_data.port)
+ val password = res.string(private_data.password)
Info(name, port, password)
}
).sortBy(_.name)
@@ -397,12 +397,12 @@
existing_server: Boolean = false,
log: Logger = No_Logger
): (Info, Option[Server]) = {
- using(SQLite.open_database(Data.database, restrict = true)) { db =>
- Data.transaction_lock(db, create = true) {
+ using(SQLite.open_database(private_data.database, restrict = true)) { db =>
+ private_data.transaction_lock(db, create = true) {
list(db).filterNot(_.active).foreach(server_info =>
- db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))
+ db.execute_statement(private_data.table.delete(sql = private_data.name.where_equal(server_info.name))))
}
- Data.transaction_lock(db) {
+ private_data.transaction_lock(db) {
find(db, name) match {
case Some(server_info) => (server_info, None)
case None =>
@@ -411,8 +411,8 @@
val server = new Server(port, log)
val server_info = Info(name, server.port, server.password)
- db.execute_statement(Data.table.delete(sql = Data.name.where_equal(name)))
- db.execute_statement(Data.table.insert(), body =
+ db.execute_statement(private_data.table.delete(sql = private_data.name.where_equal(name)))
+ db.execute_statement(private_data.table.insert(), body =
{ stmt =>
stmt.string(1) = server_info.name
stmt.int(2) = server_info.port
@@ -427,8 +427,8 @@
}
def exit(name: String = default_name): Boolean = {
- using(SQLite.open_database(Data.database)) { db =>
- Data.transaction_lock(db) {
+ using(SQLite.open_database(private_data.database)) { db =>
+ private_data.transaction_lock(db) {
find(db, name) match {
case Some(server_info) =>
using(server_info.connection())(_.write_line_message("shutdown"))
@@ -481,7 +481,7 @@
if (operation_list) {
for {
- server_info <- using(SQLite.open_database(Data.database))(list)
+ server_info <- using(SQLite.open_database(private_data.database))(list)
if server_info.active
} Output.writeln(server_info.toString, stdout = true)
}