src/Pure/Tools/build_process.scala

clarified signature: more explicit types;

/*  Title:      Pure/Tools/build_process.scala
    Author:     Makarius

Build process for sessions, with build database, optional heap, and
optional presentation.
*/

package isabelle


object Build_Process {
  /* timings from session database */

  object Session_Timing {
    def empty(session: String): Session_Timing = new Session_Timing(session, Time.zero, Nil)

    def load(
      session: String,
      store: Sessions.Store,
      progress: Progress = new Progress
    ): Session_Timing = {
      store.try_open_database(session) match {
        case None => empty(session)
        case Some(db) =>
          def ignore_error(msg: String) = {
            progress.echo_warning("Ignoring bad database " + db +
              " for session " + quote(session) + (if (msg == "") "" else ":\n" + msg))
            empty(session)
          }
          try {
            val command_timings = store.read_command_timings(db, session)
            val elapsed =
              store.read_session_timing(db, session) match {
                case Markup.Elapsed(s) => Time.seconds(s)
                case _ => Time.zero
              }
            new Session_Timing(session, elapsed, command_timings)
          }
          catch {
            case ERROR(msg) => ignore_error(msg)
            case exn: java.lang.Error => ignore_error(Exn.message(exn))
            case _: XML.Error => ignore_error("XML.Error")
          }
          finally { db.close() }
      }
    }
  }

  final class Session_Timing(
    val session: String,
    val elapsed: Time,
    val command_timings: List[Properties.T]
  ) {
    override def toString: String =
      session + (if (elapsed.is_relevant) " (" + elapsed.message_hms + " elapsed time)" else "")
  }
}