equal
deleted
inserted
replaced
421 |
421 |
422 def write_config(db: SQL.Database, instance: String, hostname: String, options: Options): Unit = |
422 def write_config(db: SQL.Database, instance: String, hostname: String, options: Options): Unit = |
423 db.using_statement(Config.table.insert()) { stmt => |
423 db.using_statement(Config.table.insert()) { stmt => |
424 stmt.string(1) = instance |
424 stmt.string(1) = instance |
425 stmt.string(2) = Isabelle_System.getenv("ML_IDENTIFIER") |
425 stmt.string(2) = Isabelle_System.getenv("ML_IDENTIFIER") |
426 stmt.string(3) = options.changed(Options.init(prefs = "")).mkString("\u0001") |
426 stmt.string(3) = options.make_prefs(Options.init(prefs = "")) |
427 stmt.execute() |
427 stmt.execute() |
428 } |
428 } |
429 |
429 |
430 def read_state(db: SQL.Database, instance: String): (Long, Int) = |
430 def read_state(db: SQL.Database, instance: String): (Long, Int) = |
431 db.using_statement( |
431 db.using_statement( |