more permissive: db could be empty after hard crash;
authorwenzelm
Tue Oct 31 15:15:02 2017 +0100 (18 months ago)
changeset 6695782d13ba817b2
parent 66956 696251bf6aec
child 66958 86bc3f1ec97e
more permissive: db could be empty after hard crash;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 15:13:08 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 15:15:02 2017 +0100
     1.3 @@ -959,20 +959,23 @@
     1.4  
     1.5      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     1.6      {
     1.7 -      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
     1.8 -        Session_Info.session_name.where_equal(name)))(stmt =>
     1.9 -      {
    1.10 -        val res = stmt.execute_query()
    1.11 -        if (!res.next()) None
    1.12 -        else {
    1.13 -          Some(
    1.14 -            Build.Session_Info(
    1.15 -              res.string(Session_Info.sources),
    1.16 -              split_lines(res.string(Session_Info.input_heaps)),
    1.17 -              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.18 -              res.int(Session_Info.return_code)))
    1.19 -        }
    1.20 -      })
    1.21 +      if (db.tables.contains(Session_Info.table.name)) {
    1.22 +        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.23 +          Session_Info.session_name.where_equal(name)))(stmt =>
    1.24 +        {
    1.25 +          val res = stmt.execute_query()
    1.26 +          if (!res.next()) None
    1.27 +          else {
    1.28 +            Some(
    1.29 +              Build.Session_Info(
    1.30 +                res.string(Session_Info.sources),
    1.31 +                split_lines(res.string(Session_Info.input_heaps)),
    1.32 +                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.33 +                res.int(Session_Info.return_code)))
    1.34 +          }
    1.35 +        })
    1.36 +      }
    1.37 +      else None
    1.38      }
    1.39    }
    1.40  }