src/Pure/System/host.scala
changeset 77552 080422b3d914
parent 77550 ed2f53e1552c
child 78174 cc0bd66eb498
equal deleted inserted replaced
77551:ae6df8a8685a 77552:080422b3d914
   105 
   105 
   106       val table = make_table("node_info", List(hostname, numa_next))
   106       val table = make_table("node_info", List(hostname, numa_next))
   107     }
   107     }
   108 
   108 
   109     def read_numa_next(db: SQL.Database, hostname: String): Int =
   109     def read_numa_next(db: SQL.Database, hostname: String): Int =
   110       db.using_statement(
   110       db.execute_query_statementO[Int](
   111         Node_Info.table.select(List(Node_Info.numa_next),
   111         Node_Info.table.select(List(Node_Info.numa_next),
   112           sql = Node_Info.hostname.where_equal(hostname))
   112           sql = Node_Info.hostname.where_equal(hostname)),
   113       )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_next)).nextOption.getOrElse(0))
   113         res => res.int(Node_Info.numa_next)
       
   114       ).getOrElse(0)
   114 
   115 
   115     def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
   116     def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
   116       if (read_numa_next(db, hostname) != numa_next) {
   117       if (read_numa_next(db, hostname) != numa_next) {
   117         db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
   118         db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
   118         db.execute_statement(Node_Info.table.insert(), body =
   119         db.execute_statement(Node_Info.table.insert(), body =