# HG changeset patch
# User wenzelm
# Date 1509459302 -3600
# Node ID 82d13ba817b2bbaab1b3d375363ece7700a1237c
# Parent  696251bf6aec03a2e047f0ef171e18a79776f36f
more permissive: db could be empty after hard crash;

diff -r 696251bf6aec -r 82d13ba817b2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 15:13:08 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 15:15:02 2017 +0100
@@ -959,20 +959,23 @@
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {
-      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
-        Session_Info.session_name.where_equal(name)))(stmt =>
-      {
-        val res = stmt.execute_query()
-        if (!res.next()) None
-        else {
-          Some(
-            Build.Session_Info(
-              res.string(Session_Info.sources),
-              split_lines(res.string(Session_Info.input_heaps)),
-              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
-              res.int(Session_Info.return_code)))
-        }
-      })
+      if (db.tables.contains(Session_Info.table.name)) {
+        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
+          Session_Info.session_name.where_equal(name)))(stmt =>
+        {
+          val res = stmt.execute_query()
+          if (!res.next()) None
+          else {
+            Some(
+              Build.Session_Info(
+                res.string(Session_Info.sources),
+                split_lines(res.string(Session_Info.input_heaps)),
+                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
+                res.int(Session_Info.return_code)))
+          }
+        })
+      }
+      else None
     }
   }
 }