src/Pure/Thy/sessions.scala
changeset 66746 888a51e77c6e
parent 66744 fec1504e5f03
child 66749 0445cfaf6132
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 11:43:17 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 13:33:36 2017 +0200
     1.3 @@ -815,12 +815,11 @@
     1.4        List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
     1.5  
     1.6      // Build.Session_Info
     1.7 -    val imported_sources = SQL.Column.string("imported_sources")
     1.8      val sources = SQL.Column.string("sources")
     1.9      val input_heaps = SQL.Column.string("input_heaps")
    1.10      val output_heap = SQL.Column.string("output_heap")
    1.11      val return_code = SQL.Column.int("return_code")
    1.12 -    val build_columns = List(imported_sources, sources, input_heaps, output_heap, return_code)
    1.13 +    val build_columns = List(sources, input_heaps, output_heap, return_code)
    1.14  
    1.15      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    1.16    }
    1.17 @@ -909,11 +908,10 @@
    1.18            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.19            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.20            stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
    1.21 -          stmt.string(7) = cat_lines(build.imported_sources)
    1.22 -          stmt.string(8) = cat_lines(build.sources)
    1.23 -          stmt.string(9) = cat_lines(build.input_heaps)
    1.24 -          stmt.string(10) = build.output_heap getOrElse ""
    1.25 -          stmt.int(11) = build.return_code
    1.26 +          stmt.string(7) = cat_lines(build.sources)
    1.27 +          stmt.string(8) = cat_lines(build.input_heaps)
    1.28 +          stmt.string(9) = build.output_heap getOrElse ""
    1.29 +          stmt.int(10) = build.return_code
    1.30            stmt.execute()
    1.31          })
    1.32        }
    1.33 @@ -936,34 +934,20 @@
    1.34  
    1.35      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.36      {
    1.37 -      val result0 =
    1.38 -        db.using_statement(Session_Info.table.select(Session_Info.build_columns.tail,
    1.39 -          Session_Info.session_name.where_equal(name)))(stmt =>
    1.40 -        {
    1.41 -          val res = stmt.execute_query()
    1.42 -          if (!res.next()) None
    1.43 -          else {
    1.44 -            Some(
    1.45 -              Build.Session_Info(Nil,
    1.46 -                split_lines(res.string(Session_Info.sources)),
    1.47 -                split_lines(res.string(Session_Info.input_heaps)),
    1.48 -                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.49 -                res.int(Session_Info.return_code)))
    1.50 -          }
    1.51 -        })
    1.52 -      result0.map(info =>
    1.53 -        info.copy(imported_sources =
    1.54 -          try {
    1.55 -            db.using_statement(Session_Info.table.select(List(Session_Info.imported_sources),
    1.56 -              Session_Info.session_name.where_equal(name)))(stmt =>
    1.57 -            {
    1.58 -              val res = stmt.execute_query()
    1.59 -              if (!res.next) Nil else split_lines(res.string(Session_Info.imported_sources))
    1.60 -            })
    1.61 -          } // column "imported_sources" could be missing
    1.62 -          catch { case _: java.sql.SQLException => Nil }
    1.63 -        )
    1.64 -      )
    1.65 +      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.66 +        Session_Info.session_name.where_equal(name)))(stmt =>
    1.67 +      {
    1.68 +        val res = stmt.execute_query()
    1.69 +        if (!res.next()) None
    1.70 +        else {
    1.71 +          Some(
    1.72 +            Build.Session_Info(
    1.73 +              split_lines(res.string(Session_Info.sources)),
    1.74 +              split_lines(res.string(Session_Info.input_heaps)),
    1.75 +              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.76 +              res.int(Session_Info.return_code)))
    1.77 +        }
    1.78 +      })
    1.79      }
    1.80    }
    1.81  }