src/Pure/Tools/build_process.scala
author wenzelm
Sat, 11 Feb 2023 12:09:42 +0100
changeset 77239 b9bf4c0bd47d
parent 77238 02308a0ddf30
child 77240 2ff94ba22140
permissions -rw-r--r--
clarified signature: more explicit types;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_process.scala
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     3
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     4
Build process for sessions, with build database, optional heap, and
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     5
optional presentation.
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     6
*/
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     7
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     8
package isabelle
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     9
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    10
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    11
object Build_Process {
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    12
  /* timings from session database */
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    13
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    14
  object Session_Timing {
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    15
    def empty(session: String): Session_Timing = new Session_Timing(session, Time.zero, Nil)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    16
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    17
    def load(
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    18
      session: String,
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    19
      store: Sessions.Store,
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    20
      progress: Progress = new Progress
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    21
    ): Session_Timing = {
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    22
      store.try_open_database(session) match {
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    23
        case None => empty(session)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    24
        case Some(db) =>
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    25
          def ignore_error(msg: String) = {
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    26
            progress.echo_warning("Ignoring bad database " + db +
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    27
              " for session " + quote(session) + (if (msg == "") "" else ":\n" + msg))
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    28
            empty(session)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    29
          }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    30
          try {
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    31
            val command_timings = store.read_command_timings(db, session)
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    32
            val elapsed =
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    33
              store.read_session_timing(db, session) match {
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    34
                case Markup.Elapsed(s) => Time.seconds(s)
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    35
                case _ => Time.zero
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    36
              }
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    37
            new Session_Timing(session, elapsed, command_timings)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    38
          }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    39
          catch {
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    40
            case ERROR(msg) => ignore_error(msg)
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    41
            case exn: java.lang.Error => ignore_error(Exn.message(exn))
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    42
            case _: XML.Error => ignore_error("XML.Error")
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    43
          }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    44
          finally { db.close() }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    45
      }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    46
    }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    47
  }
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    48
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    49
  final class Session_Timing(
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    50
    val session: String,
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    51
    val elapsed: Time,
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    52
    val command_timings: List[Properties.T]
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    53
  ) {
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    54
    override def toString: String =
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    55
      session + (if (elapsed.is_relevant) " (" + elapsed.message_hms + " elapsed time)" else "")
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    56
  }
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    57
}