tuned;
authorwenzelm
Sun Mar 19 14:06:45 2017 +0100 (2017-03-19)
changeset 653241964d3cb2e57
parent 65323 7f6c738379f4
child 65325 981df08de0ab
tuned;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Mar 19 13:47:07 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Mar 19 14:06:45 2017 +0100
     1.3 @@ -586,7 +586,7 @@
     1.4        using(Session_Info.select_statement(db, name, List(column)))(stmt =>
     1.5        {
     1.6          val rs = stmt.executeQuery
     1.7 -        if (!rs.next) Bytes.empty else db.bytes(rs, column.name)
     1.8 +        if (!rs.next) Bytes.empty else db.bytes(rs, column)
     1.9        })
    1.10  
    1.11      def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
    1.12 @@ -689,11 +689,10 @@
    1.13          else {
    1.14            Some(
    1.15              Build.Session_Info(
    1.16 -              split_lines(db.string(rs, Session_Info.sources.name)),
    1.17 -              split_lines(db.string(rs, Session_Info.input_heaps.name)),
    1.18 -              db.string(rs,
    1.19 -                Session_Info.output_heap.name) match { case "" => None case s => Some(s) },
    1.20 -              db.int(rs, Session_Info.return_code.name)))
    1.21 +              split_lines(db.string(rs, Session_Info.sources)),
    1.22 +              split_lines(db.string(rs, Session_Info.input_heaps)),
    1.23 +              db.string(rs, Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.24 +              db.int(rs, Session_Info.return_code)))
    1.25          }
    1.26        })
    1.27    }