tuned;
authorwenzelm
Sun, 19 Mar 2017 14:06:45 +0100
changeset 65324 1964d3cb2e57
parent 65323 7f6c738379f4
child 65325 981df08de0ab
tuned;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Mar 19 13:47:07 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Mar 19 14:06:45 2017 +0100
@@ -586,7 +586,7 @@
       using(Session_Info.select_statement(db, name, List(column)))(stmt =>
       {
         val rs = stmt.executeQuery
-        if (!rs.next) Bytes.empty else db.bytes(rs, column.name)
+        if (!rs.next) Bytes.empty else db.bytes(rs, column)
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
@@ -689,11 +689,10 @@
         else {
           Some(
             Build.Session_Info(
-              split_lines(db.string(rs, Session_Info.sources.name)),
-              split_lines(db.string(rs, Session_Info.input_heaps.name)),
-              db.string(rs,
-                Session_Info.output_heap.name) match { case "" => None case s => Some(s) },
-              db.int(rs, Session_Info.return_code.name)))
+              split_lines(db.string(rs, Session_Info.sources)),
+              split_lines(db.string(rs, Session_Info.input_heaps)),
+              db.string(rs, Session_Info.output_heap) match { case "" => None case s => Some(s) },
+              db.int(rs, Session_Info.return_code)))
         }
       })
   }