62 } |
62 } |
63 else Path.make(elems.drop(prune)) |
63 else Path.make(elems.drop(prune)) |
64 } |
64 } |
65 |
65 |
66 def readable(db: SQL.Database): Boolean = { |
66 def readable(db: SQL.Database): Boolean = { |
67 val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name)) |
67 db.using_statement( |
68 db.using_statement(select)(stmt => stmt.execute_query().next()) |
68 Data.table.select(List(Data.name), |
69 } |
69 sql = Data.where_equal(session, theory, name)))(_.execute_query().next()) |
70 |
70 } |
71 def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = { |
71 |
72 val select = |
72 def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = |
|
73 db.using_statement( |
73 Data.table.select(List(Data.executable, Data.compressed, Data.body), |
74 Data.table.select(List(Data.executable, Data.compressed, Data.body), |
74 Data.where_equal(session, theory, name)) |
75 sql = Data.where_equal(session, theory, name))) { stmt => |
75 db.using_statement(select) { stmt => |
|
76 val res = stmt.execute_query() |
76 val res = stmt.execute_query() |
77 if (res.next()) { |
77 if (res.next()) { |
78 val executable = res.bool(Data.executable) |
78 val executable = res.bool(Data.executable) |
79 val compressed = res.bool(Data.compressed) |
79 val compressed = res.bool(Data.compressed) |
80 val bytes = res.bytes(Data.body) |
80 val bytes = res.bytes(Data.body) |
81 val body = Future.value(compressed, bytes) |
81 val body = Future.value(compressed, bytes) |
82 Some(Entry(this, executable, body, cache)) |
82 Some(Entry(this, executable, body, cache)) |
83 } |
83 } |
84 else None |
84 else None |
85 } |
85 } |
86 } |
86 } |
87 } |
87 |
88 |
88 def read_theory_names(db: SQL.Database, session_name: String): List[String] = |
89 def read_theory_names(db: SQL.Database, session_name: String): List[String] = { |
89 db.using_statement( |
90 val select = |
90 Data.table.select(List(Data.theory_name), distinct = true, |
91 Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) + |
91 sql = Data.where_equal(session_name) + SQL.order_by(List(Data.theory_name))) |
92 SQL.order_by(List(Data.theory_name)) |
92 ) { stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList } |
93 db.using_statement(select)(stmt => |
93 |
94 stmt.execute_query().iterator(_.string(Data.theory_name)).toList) |
94 def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = |
95 } |
95 db.using_statement( |
96 |
96 Data.table.select(List(Data.theory_name, Data.name), |
97 def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = { |
97 sql = Data.where_equal(session_name)) + SQL.order_by(List(Data.theory_name, Data.name)) |
98 val select = |
98 ) { stmt => |
99 Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) + |
99 stmt.execute_query().iterator(res => |
100 SQL.order_by(List(Data.theory_name, Data.name)) |
100 Entry_Name(session = session_name, |
101 db.using_statement(select)(stmt => |
101 theory = res.string(Data.theory_name), |
102 stmt.execute_query().iterator(res => |
102 name = res.string(Data.name))).toList |
103 Entry_Name(session = session_name, |
103 } |
104 theory = res.string(Data.theory_name), |
|
105 name = res.string(Data.name))).toList) |
|
106 } |
|
107 |
104 |
108 def message(msg: String, theory_name: String, name: String): String = |
105 def message(msg: String, theory_name: String, name: String): String = |
109 msg + " " + quote(name) + " for theory " + quote(theory_name) |
106 msg + " " + quote(name) + " for theory " + quote(theory_name) |
110 |
107 |
111 object Entry { |
108 object Entry { |