# HG changeset patch
# User wenzelm
# Date 1489928805 -3600
# Node ID 1964d3cb2e5789932066a4aedc10b8678932b697
# Parent  7f6c738379f42093d8e0f9037b73399be000e6ae
tuned;

diff -r 7f6c738379f4 -r 1964d3cb2e57 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)))
         }
       })
   }