src/Pure/Tools/server.scala

--- 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)
         }