merged
authorwenzelm
Fri Mar 17 23:24:04 2017 +0100 (2017-03-17)
changeset 652996b840c704441
parent 65274 db2de50de28e
parent 65298 9cbc44f8e0d8
child 65300 c262653a3b88
merged
     1.1 --- a/src/Pure/Admin/build_history.scala	Thu Mar 16 16:02:18 2017 +0000
     1.2 +++ b/src/Pure/Admin/build_history.scala	Fri Mar 17 23:24:04 2017 +0100
     1.3 @@ -207,6 +207,8 @@
     1.4  
     1.5        /* output log */
     1.6  
     1.7 +      val store = Sessions.store()
     1.8 +
     1.9        val meta_info =
    1.10          Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
    1.11          Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args1) :::
    1.12 @@ -222,12 +224,20 @@
    1.13        val ml_statistics =
    1.14          build_info.finished_sessions.flatMap(session_name =>
    1.15            {
    1.16 -            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
    1.17 -            if (session_log.is_file) {
    1.18 -              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
    1.19 -                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
    1.20 -            }
    1.21 -            else Nil
    1.22 +            val database = isabelle_output + store.database(session_name)
    1.23 +            val log_gz = isabelle_output + store.log_gz(session_name)
    1.24 +
    1.25 +            val properties =
    1.26 +              if (database.is_file) {
    1.27 +                using(SQLite.open_database(database))(db =>
    1.28 +                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
    1.29 +              }
    1.30 +              else if (log_gz.is_file) {
    1.31 +                Build_Log.Log_File(log_gz).
    1.32 +                  parse_session_info(session_name, ml_statistics = true).ml_statistics
    1.33 +              }
    1.34 +              else Nil
    1.35 +            properties.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
    1.36            })
    1.37  
    1.38        val heap_sizes =
     2.1 --- a/src/Pure/Admin/build_log.scala	Thu Mar 16 16:02:18 2017 +0000
     2.2 +++ b/src/Pure/Admin/build_log.scala	Fri Mar 17 23:24:04 2017 +0100
     2.3 @@ -265,7 +265,7 @@
     2.4  
     2.5  
     2.6  
     2.7 -  /** meta info **/
     2.8 +  /** digested meta info: produced by Admin/build_history in log.xz file **/
     2.9  
    2.10    object Meta_Info
    2.11    {
    2.12 @@ -379,7 +379,7 @@
    2.13  
    2.14  
    2.15  
    2.16 -  /** build info: produced by isabelle build or build_history **/
    2.17 +  /** build info: toplevel output of isabelle build or Admin/build_history **/
    2.18  
    2.19    val ML_STATISTICS_MARKER = "\fML_statistics = "
    2.20    val SESSION_NAME = "session_name"
    2.21 @@ -539,7 +539,7 @@
    2.22  
    2.23  
    2.24  
    2.25 -  /** session info: produced by "isabelle build" **/
    2.26 +  /** session info: produced by isabelle build as session log.gz file **/
    2.27  
    2.28    sealed case class Session_Info(
    2.29      session_name: String,
    2.30 @@ -555,22 +555,16 @@
    2.31      ml_statistics: Boolean,
    2.32      task_statistics: Boolean): Session_Info =
    2.33    {
    2.34 -    val xml_cache = new XML.Cache()
    2.35 -
    2.36 -    val session_name =
    2.37 -      log_file.find_line("\fSession.name = ") match {
    2.38 -        case None => default_name
    2.39 -        case Some(name) if default_name == "" || default_name == name => name
    2.40 -        case Some(name) => log_file.err("log from different session " + quote(name))
    2.41 -      }
    2.42 -    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
    2.43 -    val command_timings_ =
    2.44 -      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
    2.45 -    val ml_statistics_ =
    2.46 -      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
    2.47 -    val task_statistics_ =
    2.48 -      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
    2.49 -
    2.50 -    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
    2.51 +    Session_Info(
    2.52 +      session_name =
    2.53 +        log_file.find_line("\fSession.name = ") match {
    2.54 +          case None => default_name
    2.55 +          case Some(name) if default_name == "" || default_name == name => name
    2.56 +          case Some(name) => log_file.err("log from different session " + quote(name))
    2.57 +        },
    2.58 +      session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
    2.59 +      command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
    2.60 +      ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
    2.61 +      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
    2.62    }
    2.63  }
     3.1 --- a/src/Pure/General/bytes.scala	Thu Mar 16 16:02:18 2017 +0000
     3.2 +++ b/src/Pure/General/bytes.scala	Fri Mar 17 23:24:04 2017 +0100
     3.3 @@ -110,9 +110,12 @@
     3.4  
     3.5    lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
     3.6  
     3.7 +  def text: String =
     3.8 +    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
     3.9 +
    3.10    override def toString: String =
    3.11    {
    3.12 -    val str = UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
    3.13 +    val str = text
    3.14      if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
    3.15    }
    3.16  
     4.1 --- a/src/Pure/General/exn.scala	Thu Mar 16 16:02:18 2017 +0000
     4.2 +++ b/src/Pure/General/exn.scala	Fri Mar 17 23:24:04 2017 +0100
     4.3 @@ -20,7 +20,7 @@
     4.4        }
     4.5      override def hashCode: Int = message.hashCode
     4.6  
     4.7 -    override def toString: String = Output.error_text(message)
     4.8 +    override def toString: String = "\n" + Output.error_text(message)
     4.9    }
    4.10  
    4.11    object ERROR
     5.1 --- a/src/Pure/General/sql.scala	Thu Mar 16 16:02:18 2017 +0000
     5.2 +++ b/src/Pure/General/sql.scala	Fri Mar 17 23:24:04 2017 +0100
     5.3 @@ -68,24 +68,24 @@
     5.4  
     5.5    object Column
     5.6    {
     5.7 -    def bool(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
     5.8 +    def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
     5.9        Column(name, Type.Boolean, strict, primary_key)
    5.10 -    def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    5.11 +    def int(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    5.12        Column(name, Type.Int, strict, primary_key)
    5.13 -    def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    5.14 +    def long(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    5.15        Column(name, Type.Long, strict, primary_key)
    5.16 -    def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    5.17 +    def double(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    5.18        Column(name, Type.Double, strict, primary_key)
    5.19 -    def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    5.20 +    def string(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    5.21        Column(name, Type.String, strict, primary_key)
    5.22 -    def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    5.23 +    def bytes(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    5.24        Column(name, Type.Bytes, strict, primary_key)
    5.25 -    def date(name: String, strict: Boolean = true, primary_key: Boolean = false): Column =
    5.26 +    def date(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
    5.27        Column(name, Type.Date, strict, primary_key)
    5.28    }
    5.29  
    5.30    sealed case class Column(
    5.31 -    name: String, T: Type.Value, strict: Boolean = true, primary_key: Boolean = false)
    5.32 +    name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false)
    5.33    {
    5.34      def sql_name: String = quote_ident(name)
    5.35      def sql_decl(sql_type: Type.Value => String): String =
    5.36 @@ -240,17 +240,17 @@
    5.37      def tables: List[String] =
    5.38        iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
    5.39  
    5.40 -    def create_table(table: Table, strict: Boolean = true, rowid: Boolean = true): Unit =
    5.41 +    def create_table(table: Table, strict: Boolean = false, rowid: Boolean = true): Unit =
    5.42        using(statement(table.sql_create(strict, rowid, sql_type)))(_.execute())
    5.43  
    5.44 -    def drop_table(table: Table, strict: Boolean = true): Unit =
    5.45 +    def drop_table(table: Table, strict: Boolean = false): Unit =
    5.46        using(statement(table.sql_drop(strict)))(_.execute())
    5.47  
    5.48      def create_index(table: Table, name: String, columns: List[Column],
    5.49 -        strict: Boolean = true, unique: Boolean = false): Unit =
    5.50 +        strict: Boolean = false, unique: Boolean = false): Unit =
    5.51        using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
    5.52  
    5.53 -    def drop_index(table: Table, name: String, strict: Boolean = true): Unit =
    5.54 +    def drop_index(table: Table, name: String, strict: Boolean = false): Unit =
    5.55        using(statement(table.sql_drop_index(name, strict)))(_.execute())
    5.56    }
    5.57  }
    5.58 @@ -264,8 +264,11 @@
    5.59    // see https://www.sqlite.org/lang_datefunc.html
    5.60    val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x")
    5.61  
    5.62 +  lazy val init_jdbc: Unit = Class.forName("org.sqlite.JDBC")
    5.63 +
    5.64    def open_database(path: Path): Database =
    5.65    {
    5.66 +    init_jdbc
    5.67      val path0 = path.expand
    5.68      val s0 = File.platform_path(path0)
    5.69      val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
    5.70 @@ -296,6 +299,8 @@
    5.71  {
    5.72    val default_port = 5432
    5.73  
    5.74 +  lazy val init_jdbc: Unit = Class.forName("org.postgresql.Driver")
    5.75 +
    5.76    def open_database(
    5.77      user: String,
    5.78      password: String,
    5.79 @@ -304,6 +309,8 @@
    5.80      port: Int = default_port,
    5.81      ssh: Option[SSH.Session] = None): Database =
    5.82    {
    5.83 +    init_jdbc
    5.84 +
    5.85      require(user != "")
    5.86  
    5.87      val db_host = if (host != "") host else "localhost"
     6.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 16 16:02:18 2017 +0000
     6.2 +++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 23:24:04 2017 +0100
     6.3 @@ -515,13 +515,80 @@
     6.4  
     6.5    /** persistent store **/
     6.6  
     6.7 -  def log(name: String): Path = Path.basic("log") + Path.basic(name)
     6.8 -  def log_gz(name: String): Path = log(name).ext("gz")
     6.9 +  object Session_Info
    6.10 +  {
    6.11 +    // Build_Log.Session_Info
    6.12 +    val session_name = SQL.Column.string("session_name")
    6.13 +    val session_timing = SQL.Column.bytes("session_timing")
    6.14 +    val command_timings = SQL.Column.bytes("command_timings")
    6.15 +    val ml_statistics = SQL.Column.bytes("ml_statistics")
    6.16 +    val task_statistics = SQL.Column.bytes("task_statistics")
    6.17 +    val build_log_columns =
    6.18 +      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    6.19 +
    6.20 +    // Build.Session_Info
    6.21 +    val sources = SQL.Column.string("sources")
    6.22 +    val input_heaps = SQL.Column.string("input_heaps")
    6.23 +    val output_heap = SQL.Column.string("output_heap")
    6.24 +    val return_code = SQL.Column.int("return_code")
    6.25 +    val build_columns = List(sources, input_heaps, output_heap, return_code)
    6.26 +
    6.27 +    val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    6.28 +  }
    6.29  
    6.30    def store(system_mode: Boolean = false): Store = new Store(system_mode)
    6.31  
    6.32    class Store private[Sessions](system_mode: Boolean)
    6.33    {
    6.34 +    /* file names */
    6.35 +
    6.36 +    def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
    6.37 +    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    6.38 +    def log_gz(name: String): Path = log(name).ext("gz")
    6.39 +
    6.40 +
    6.41 +    /* SQL database content */
    6.42 +
    6.43 +    val xml_cache: XML.Cache = new XML.Cache()
    6.44 +
    6.45 +    def encode_properties(ps: Properties.T): Bytes =
    6.46 +      Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    6.47 +
    6.48 +    def decode_properties(bs: Bytes): Properties.T =
    6.49 +      xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
    6.50 +
    6.51 +    def compress_properties(ps: List[Properties.T], options: XZ.Options = XZ.options()): Bytes =
    6.52 +    {
    6.53 +      if (ps.isEmpty) Bytes.empty
    6.54 +      else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
    6.55 +    }
    6.56 +
    6.57 +    def uncompress_properties(bs: Bytes): List[Properties.T] =
    6.58 +    {
    6.59 +      if (bs.isEmpty) Nil
    6.60 +      else
    6.61 +        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)).
    6.62 +          map(xml_cache.props(_))
    6.63 +    }
    6.64 +
    6.65 +    def read_string(db: SQL.Database, table: SQL.Table, column: SQL.Column): String =
    6.66 +      using(db.select_statement(table, List(column)))(stmt =>
    6.67 +      {
    6.68 +        val rs = stmt.executeQuery
    6.69 +        if (!rs.next) "" else db.string(rs, column.name)
    6.70 +      })
    6.71 +
    6.72 +    def read_bytes(db: SQL.Database, table: SQL.Table, column: SQL.Column): Bytes =
    6.73 +      using(db.select_statement(table, List(column)))(stmt =>
    6.74 +      {
    6.75 +        val rs = stmt.executeQuery
    6.76 +        if (!rs.next) Bytes.empty else db.bytes(rs, column.name)
    6.77 +      })
    6.78 +
    6.79 +    def read_properties(db: SQL.Database, table: SQL.Table, column: SQL.Column)
    6.80 +      : List[Properties.T] = uncompress_properties(read_bytes(db, table, column))
    6.81 +
    6.82 +
    6.83      /* output */
    6.84  
    6.85      val browser_info: Path =
    6.86 @@ -532,6 +599,8 @@
    6.87        if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
    6.88        else Path.explode("$ISABELLE_OUTPUT")
    6.89  
    6.90 +    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
    6.91 +
    6.92      def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    6.93  
    6.94  
    6.95 @@ -544,22 +613,87 @@
    6.96          output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
    6.97        }
    6.98  
    6.99 -    def find(name: String): Option[(Path, Option[String])] =
   6.100 -      input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
   6.101 -        (dir + log_gz(name), read_heap_digest(dir + Path.basic(name))))
   6.102 +    def find_database_heap(name: String): Option[(Path, Option[String])] =
   6.103 +      input_dirs.find(dir => (dir + database(name)).is_file).map(dir =>
   6.104 +        (dir + database(name), read_heap_digest(dir + Path.basic(name))))
   6.105  
   6.106 -    def find_log(name: String): Option[Path] =
   6.107 -      input_dirs.map(_ + log(name)).find(_.is_file)
   6.108 -
   6.109 -    def find_log_gz(name: String): Option[Path] =
   6.110 -      input_dirs.map(_ + log_gz(name)).find(_.is_file)
   6.111 -
   6.112 -    def find_heap(name: String): Option[Path] =
   6.113 -      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
   6.114 +    def find_database(name: String): Option[Path] =
   6.115 +      input_dirs.map(_ + database(name)).find(_.is_file)
   6.116  
   6.117      def heap(name: String): Path =
   6.118 -      find_heap(name) getOrElse
   6.119 +      input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
   6.120          error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
   6.121            cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
   6.122 +
   6.123 +
   6.124 +    /* session info */
   6.125 +
   6.126 +    def write_session_info(
   6.127 +      db: SQL.Database, build_log: Build_Log.Session_Info, build: Build.Session_Info)
   6.128 +    {
   6.129 +      db.transaction {
   6.130 +        db.drop_table(Session_Info.table)
   6.131 +        db.create_table(Session_Info.table)
   6.132 +        using(db.insert_statement(Session_Info.table))(stmt =>
   6.133 +        {
   6.134 +          db.set_string(stmt, 1, build_log.session_name)
   6.135 +          db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
   6.136 +          db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
   6.137 +          db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
   6.138 +          db.set_bytes(stmt, 5, compress_properties(build_log.task_statistics))
   6.139 +          db.set_string(stmt, 6, cat_lines(build.sources))
   6.140 +          db.set_string(stmt, 7, cat_lines(build.input_heaps))
   6.141 +          db.set_string(stmt, 8, build.output_heap getOrElse "")
   6.142 +          db.set_int(stmt, 9, build.return_code)
   6.143 +          stmt.execute()
   6.144 +        })
   6.145 +      }
   6.146 +    }
   6.147 +
   6.148 +    def read_session_timing(db: SQL.Database): Properties.T =
   6.149 +      decode_properties(read_bytes(db, Session_Info.table, Session_Info.session_timing))
   6.150 +
   6.151 +    def read_command_timings(db: SQL.Database): List[Properties.T] =
   6.152 +      read_properties(db, Session_Info.table, Session_Info.command_timings)
   6.153 +
   6.154 +    def read_ml_statistics(db: SQL.Database): List[Properties.T] =
   6.155 +      read_properties(db, Session_Info.table, Session_Info.ml_statistics)
   6.156 +
   6.157 +    def read_task_statistics(db: SQL.Database): List[Properties.T] =
   6.158 +      read_properties(db, Session_Info.table, Session_Info.task_statistics)
   6.159 +
   6.160 +    def read_build_log(db: SQL.Database,
   6.161 +      default_name: String = "",
   6.162 +      command_timings: Boolean = false,
   6.163 +      ml_statistics: Boolean = false,
   6.164 +      task_statistics: Boolean = false): Build_Log.Session_Info =
   6.165 +    {
   6.166 +      val name = read_string(db, Session_Info.table, Session_Info.session_name)
   6.167 +      Build_Log.Session_Info(
   6.168 +        session_name =
   6.169 +          if (name == "") default_name
   6.170 +          else if (default_name == "" || default_name == name) name
   6.171 +          else error("Database from different session " + quote(name)),
   6.172 +        session_timing = read_session_timing(db),
   6.173 +        command_timings = if (command_timings) read_command_timings(db) else Nil,
   6.174 +        ml_statistics = if (ml_statistics) read_ml_statistics(db) else Nil,
   6.175 +        task_statistics = if (task_statistics) read_task_statistics(db) else Nil)
   6.176 +    }
   6.177 +
   6.178 +    def read_build(db: SQL.Database): Option[Build.Session_Info] =
   6.179 +      using(db.select_statement(Session_Info.table, Session_Info.build_columns))(stmt =>
   6.180 +      {
   6.181 +        val rs = stmt.executeQuery
   6.182 +        if (!rs.next) None
   6.183 +        else {
   6.184 +          Some(
   6.185 +            Build.Session_Info(
   6.186 +              split_lines(db.string(rs, Session_Info.sources.name)),
   6.187 +              split_lines(db.string(rs, Session_Info.input_heaps.name)),
   6.188 +              db.string(rs,
   6.189 +                Session_Info.output_heap.name) match { case "" => None case s => Some(s) },
   6.190 +              db.int(rs, Session_Info.return_code.name)))
   6.191 +        }
   6.192 +      })
   6.193    }
   6.194  }
     7.1 --- a/src/Pure/Tools/build.scala	Thu Mar 16 16:02:18 2017 +0000
     7.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 23:24:04 2017 +0100
     7.3 @@ -21,16 +21,53 @@
     7.4  {
     7.5    /** auxiliary **/
     7.6  
     7.7 -  /* queue */
     7.8 +  /* persistent build info */
     7.9 +
    7.10 +  sealed case class Session_Info(
    7.11 +    sources: List[String],
    7.12 +    input_heaps: List[String],
    7.13 +    output_heap: Option[String],
    7.14 +    return_code: Int)
    7.15 +
    7.16 +
    7.17 +  /* queue with scheduling information */
    7.18  
    7.19    private object Queue
    7.20    {
    7.21 -    def apply(tree: Sessions.Tree, load_timings: String => (List[Properties.T], Double)): Queue =
    7.22 +    def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) =
    7.23 +    {
    7.24 +      val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    7.25 +
    7.26 +      store.find_database(name) match {
    7.27 +        case None => no_timings
    7.28 +        case Some(database) =>
    7.29 +          def ignore_error(msg: String) =
    7.30 +          {
    7.31 +            Output.warning("Ignoring bad database: " + database + (if (msg == "") "" else "\n" + msg))
    7.32 +            no_timings
    7.33 +          }
    7.34 +          try {
    7.35 +            using(SQLite.open_database(database))(db =>
    7.36 +            {
    7.37 +              val build_log = store.read_build_log(db, name, command_timings = true)
    7.38 +              val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    7.39 +              (build_log.command_timings, session_timing)
    7.40 +            })
    7.41 +          }
    7.42 +          catch {
    7.43 +            case ERROR(msg) => ignore_error(msg)
    7.44 +            case exn: java.lang.Error => ignore_error(Exn.message(exn))
    7.45 +            case _: XML.Error => ignore_error("")
    7.46 +          }
    7.47 +      }
    7.48 +    }
    7.49 +
    7.50 +    def apply(tree: Sessions.Tree, store: Sessions.Store): Queue =
    7.51      {
    7.52        val graph = tree.graph
    7.53        val sessions = graph.keys
    7.54  
    7.55 -      val timings = Par_List.map((name: String) => (name, load_timings(name)), sessions)
    7.56 +      val timings = sessions.map(name => (name, load_timings(store, name)))
    7.57        val command_timings =
    7.58          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    7.59        val session_timing =
    7.60 @@ -201,46 +238,6 @@
    7.61    }
    7.62  
    7.63  
    7.64 -  /* sources and heaps */
    7.65 -
    7.66 -  private val SOURCES = "sources: "
    7.67 -  private val INPUT_HEAP = "input_heap: "
    7.68 -  private val OUTPUT_HEAP = "output_heap: "
    7.69 -  private val LOG_START = "log:"
    7.70 -  private val line_prefixes = List(SOURCES, INPUT_HEAP, OUTPUT_HEAP, LOG_START)
    7.71 -
    7.72 -  private def sources_stamp(digests: List[SHA1.Digest]): String =
    7.73 -    digests.map(_.toString).sorted.mkString(SOURCES, " ", "")
    7.74 -
    7.75 -  private def read_stamps(path: Path): Option[(String, List[String], List[String])] =
    7.76 -    if (path.is_file) {
    7.77 -      val stream = new GZIPInputStream(new BufferedInputStream(new FileInputStream(path.file)))
    7.78 -      val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
    7.79 -      val lines =
    7.80 -      {
    7.81 -        val lines = new mutable.ListBuffer[String]
    7.82 -        try {
    7.83 -          var finished = false
    7.84 -          while (!finished) {
    7.85 -            val line = reader.readLine
    7.86 -            if (line != null && line_prefixes.exists(line.startsWith(_)))
    7.87 -              lines += line
    7.88 -            else finished = true
    7.89 -          }
    7.90 -        }
    7.91 -        finally { reader.close }
    7.92 -        lines.toList
    7.93 -      }
    7.94 -
    7.95 -      if (!lines.isEmpty && lines.last.startsWith(LOG_START)) {
    7.96 -        lines.find(_.startsWith(SOURCES)).map(s =>
    7.97 -          (s, lines.filter(_.startsWith(INPUT_HEAP)), lines.filter(_.startsWith(OUTPUT_HEAP))))
    7.98 -      }
    7.99 -      else None
   7.100 -    }
   7.101 -    else None
   7.102 -
   7.103 -
   7.104  
   7.105    /** build with results **/
   7.106  
   7.107 @@ -323,56 +320,22 @@
   7.108      val deps =
   7.109        Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   7.110  
   7.111 -    def session_sources_stamp(name: String): String =
   7.112 -      sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))
   7.113 -
   7.114 -    val store = Sessions.store(system_mode)
   7.115 -
   7.116 -
   7.117 -    /* queue with scheduling information */
   7.118 -
   7.119 -    def load_timings(name: String): (List[Properties.T], Double) =
   7.120 -    {
   7.121 -      val (path, text) =
   7.122 -        store.find_log_gz(name) match {
   7.123 -          case Some(path) => (path, File.read_gzip(path))
   7.124 -          case None =>
   7.125 -            store.find_log(name) match {
   7.126 -              case Some(path) => (path, File.read(path))
   7.127 -              case None => (Path.current, "")
   7.128 -            }
   7.129 -        }
   7.130 -
   7.131 -      def ignore_error(msg: String): (List[Properties.T], Double) =
   7.132 -      {
   7.133 -        Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg))
   7.134 -        (Nil, 0.0)
   7.135 -      }
   7.136 -
   7.137 -      try {
   7.138 -        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
   7.139 -        val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
   7.140 -        (info.command_timings, session_timing)
   7.141 -      }
   7.142 -      catch {
   7.143 -        case ERROR(msg) => ignore_error(msg)
   7.144 -        case exn: java.lang.Error => ignore_error(Exn.message(exn))
   7.145 -        case _: XML.Error => ignore_error("")
   7.146 -      }
   7.147 -    }
   7.148 -
   7.149 -    val queue = Queue(selected_tree, load_timings)
   7.150 +    def sources_stamp(name: String): List[String] =
   7.151 +      (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   7.152  
   7.153  
   7.154      /* main build process */
   7.155  
   7.156 +    val store = Sessions.store(system_mode)
   7.157 +    val queue = Queue(selected_tree, store)
   7.158 +
   7.159      store.prepare_output()
   7.160  
   7.161      // optional cleanup
   7.162      if (clean_build) {
   7.163        for (name <- full_tree.graph.all_succs(selected)) {
   7.164          val files =
   7.165 -          List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)).
   7.166 +          List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   7.167              map(store.output_dir + _).filter(_.is_file)
   7.168          if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   7.169          if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   7.170 @@ -422,44 +385,53 @@
   7.171              if (process_result.ok)
   7.172                progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   7.173  
   7.174 +            val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   7.175              val process_result_tail =
   7.176              {
   7.177 -              val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   7.178                val tail = job.info.options.int("process_output_tail")
   7.179 -              val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
   7.180                process_result.copy(
   7.181                  out_lines =
   7.182 -                  "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" ::
   7.183 -                  lines1)
   7.184 +                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   7.185 +                  (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   7.186              }
   7.187  
   7.188              val heap_stamp =
   7.189                if (process_result.ok) {
   7.190 -                (store.output_dir + Sessions.log(name)).file.delete
   7.191 +                (store.output_dir + store.log(name)).file.delete
   7.192                  val heap_stamp =
   7.193                    for (path <- job.output_path if path.is_file)
   7.194                      yield Sessions.write_heap_digest(path)
   7.195  
   7.196 -                File.write_gzip(store.output_dir + Sessions.log_gz(name),
   7.197 -                  terminate_lines(
   7.198 -                    session_sources_stamp(name) ::
   7.199 -                    input_heaps.map(INPUT_HEAP + _) :::
   7.200 -                    heap_stamp.toList.map(OUTPUT_HEAP + _) :::
   7.201 -                    List(LOG_START) ::: process_result.out_lines))
   7.202 +                File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
   7.203  
   7.204                  heap_stamp
   7.205                }
   7.206                else {
   7.207                  (store.output_dir + Path.basic(name)).file.delete
   7.208 -                (store.output_dir + Sessions.log_gz(name)).file.delete
   7.209 +                (store.output_dir + store.log_gz(name)).file.delete
   7.210  
   7.211 -                File.write(store.output_dir + Sessions.log(name),
   7.212 -                  terminate_lines(process_result.out_lines))
   7.213 +                File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   7.214                  progress.echo(name + " FAILED")
   7.215                  if (!process_result.interrupted) progress.echo(process_result_tail.out)
   7.216  
   7.217                  None
   7.218                }
   7.219 +
   7.220 +            // write database
   7.221 +            {
   7.222 +              val database = store.output_dir + store.database(name)
   7.223 +              database.file.delete
   7.224 +
   7.225 +              using(SQLite.open_database(database))(db =>
   7.226 +                store.write_session_info(db,
   7.227 +                  build_log =
   7.228 +                    Build_Log.Log_File(name, process_result.out_lines).
   7.229 +                      parse_session_info(name,
   7.230 +                        command_timings = true, ml_statistics = true, task_statistics = true),
   7.231 +                  build =
   7.232 +                    Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   7.233 +            }
   7.234 +
   7.235              loop(pending - name, running - name,
   7.236                results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   7.237              //}}}
   7.238 @@ -474,15 +446,16 @@
   7.239  
   7.240                  val (current, heap_stamp) =
   7.241                  {
   7.242 -                  store.find(name) match {
   7.243 -                    case Some((log_gz, heap_stamp)) =>
   7.244 -                      read_stamps(log_gz) match {
   7.245 -                        case Some((sources, input_heaps, output_heaps)) =>
   7.246 +                  store.find_database_heap(name) match {
   7.247 +                    case Some((database, heap_stamp)) =>
   7.248 +                      using(SQLite.open_database(database))(store.read_build(_)) match {
   7.249 +                        case Some(build) =>
   7.250                            val current =
   7.251 -                            sources == session_sources_stamp(name) &&
   7.252 -                            input_heaps == ancestor_heaps.map(INPUT_HEAP + _) &&
   7.253 -                            output_heaps == heap_stamp.toList.map(OUTPUT_HEAP + _) &&
   7.254 -                            !(do_output && heap_stamp.isEmpty)
   7.255 +                            build.sources == sources_stamp(name) &&
   7.256 +                            build.input_heaps == ancestor_heaps &&
   7.257 +                            build.output_heap == heap_stamp &&
   7.258 +                            !(do_output && heap_stamp.isEmpty) &&
   7.259 +                            build.return_code == 0
   7.260                            (current, heap_stamp)
   7.261                          case None => (false, None)
   7.262                        }
     8.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Mar 16 16:02:18 2017 +0000
     8.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 17 23:24:04 2017 +0100
     8.3 @@ -23,19 +23,6 @@
     8.4  
     8.5  object PIDE
     8.6  {
     8.7 -  /* plugin instance */
     8.8 -
     8.9 -  @volatile var _plugin: Plugin = null
    8.10 -
    8.11 -  def plugin: Plugin =
    8.12 -    if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
    8.13 -    else _plugin
    8.14 -
    8.15 -  def options: JEdit_Options = plugin.options
    8.16 -  def resources: JEdit_Resources = plugin.resources
    8.17 -  def session: Session = plugin.session
    8.18 -
    8.19 -
    8.20    /* semantic document content */
    8.21  
    8.22    def snapshot(view: View): Document.Snapshot = GUI_Thread.now
    8.23 @@ -54,9 +41,21 @@
    8.24        case None => error("No document view for current text area")
    8.25      }
    8.26    }
    8.27 +
    8.28 +
    8.29 +  /* plugin instance */
    8.30 +
    8.31 +  @volatile var _plugin: Plugin = null
    8.32 +
    8.33 +  def plugin: Plugin =
    8.34 +    if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
    8.35 +    else _plugin
    8.36 +
    8.37 +  def options: JEdit_Options = plugin.options
    8.38 +  def resources: JEdit_Resources = plugin.resources
    8.39 +  def session: Session = plugin.session
    8.40  }
    8.41  
    8.42 -
    8.43  class Plugin extends EBPlugin
    8.44  {
    8.45    /* options */
    8.46 @@ -415,7 +414,7 @@
    8.47  
    8.48      // adhoc patch of confusing message
    8.49      val orig_plugin_error = jEdit.getProperty("plugin-error.start-error")
    8.50 -    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin:\n{0}")
    8.51 +    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin: {0}")
    8.52  
    8.53      init_options()
    8.54      init_resources()