src/Pure/Tools/build_job.scala
author wenzelm
Fri, 03 Mar 2023 13:39:46 +0100
changeset 77493 2d5529f56124
parent 77486 032c76e04475
child 77496 f0d9f9196b9b
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_job.scala
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     3
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     4
Build job running prover process, with rudimentary PIDE session.
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     6
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     8
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
     9
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    10
import scala.collection.mutable
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
    11
import scala.util.matching.Regex
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    12
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    13
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
    14
trait Build_Job {
77349
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
    15
  def job_name: String
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
    16
  def node_info: Host.Node_Info
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
    17
  def cancel(): Unit = ()
77298
39c7d79ace34 clarified signature defaults;
wenzelm
parents: 77297
diff changeset
    18
  def is_finished: Boolean = false
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
    19
  def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77371
diff changeset
    20
  def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info)
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
    21
}
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
    22
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74755
diff changeset
    23
object Build_Job {
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
    24
  sealed case class Result(node_info: Host.Node_Info, process_result: Process_Result) {
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77371
diff changeset
    25
    def ok: Boolean = process_result.ok
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77371
diff changeset
    26
  }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77371
diff changeset
    27
77371
84ca5e036897 tuned signature;
wenzelm
parents: 77349
diff changeset
    28
  sealed case class Abstract(
77349
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
    29
    override val job_name: String,
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
    30
    override val node_info: Host.Node_Info
77349
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
    31
  ) extends Build_Job {
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
    32
    override def make_abstract: Abstract = this
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
    33
  }
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
    34
77396
f184fbac99bc clarified modules;
wenzelm
parents: 77372
diff changeset
    35
f184fbac99bc clarified modules;
wenzelm
parents: 77372
diff changeset
    36
  /* build session */
f184fbac99bc clarified modules;
wenzelm
parents: 77372
diff changeset
    37
77464
8008ce0f2488 more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
wenzelm
parents: 77463
diff changeset
    38
  def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
8008ce0f2488 more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
wenzelm
parents: 77463
diff changeset
    39
77474
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
    40
  def start_session(
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
    41
    build_context: Build_Process.Context,
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
    42
    session_background: Sessions.Background,
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
    43
    input_shasum: SHA1.Shasum,
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
    44
    node_info: Host.Node_Info
77474
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
    45
  ): Session_Job = new Session_Job(build_context, session_background, input_shasum, node_info)
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
    46
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    47
  object Session_Context {
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    48
    def load(
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    49
      name: String,
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    50
      deps: List[String],
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    51
      ancestors: List[String],
77458
403748b23f13 clarified signature: prefer static data;
wenzelm
parents: 77456
diff changeset
    52
      sources_shasum: SHA1.Shasum,
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    53
      timeout: Time,
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    54
      store: Sessions.Store,
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    55
      progress: Progress = new Progress
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    56
    ): Session_Context = {
77450
167b5095ba14 tuned signature (again);
wenzelm
parents: 77445
diff changeset
    57
      def default: Session_Context =
77458
403748b23f13 clarified signature: prefer static data;
wenzelm
parents: 77456
diff changeset
    58
        new Session_Context(name, deps, ancestors, sources_shasum, timeout, Time.zero, Bytes.empty)
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    59
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    60
      store.try_open_database(name) match {
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    61
        case None => default
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    62
        case Some(db) =>
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    63
          def ignore_error(msg: String) = {
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    64
            progress.echo_warning(
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    65
              "Ignoring bad database " + db + " for session " + quote(name) +
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    66
              if_proper(msg, ":\n" + msg))
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    67
            default
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    68
          }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    69
          try {
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    70
            val command_timings = store.read_command_timings(db, name)
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    71
            val elapsed =
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    72
              store.read_session_timing(db, name) match {
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    73
                case Markup.Elapsed(s) => Time.seconds(s)
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    74
                case _ => Time.zero
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    75
              }
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    76
            new Session_Context(
77458
403748b23f13 clarified signature: prefer static data;
wenzelm
parents: 77456
diff changeset
    77
              name, deps, ancestors, sources_shasum, timeout, elapsed, command_timings)
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    78
          }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    79
          catch {
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    80
            case ERROR(msg) => ignore_error(msg)
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    81
            case exn: java.lang.Error => ignore_error(Exn.message(exn))
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    82
            case _: XML.Error => ignore_error("XML.Error")
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    83
          }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    84
          finally { db.close() }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    85
      }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    86
    }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    87
  }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    88
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    89
  final class Session_Context(
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    90
    val name: String,
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    91
    val deps: List[String],
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    92
    val ancestors: List[String],
77458
403748b23f13 clarified signature: prefer static data;
wenzelm
parents: 77456
diff changeset
    93
    val sources_shasum: SHA1.Shasum,
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    94
    val timeout: Time,
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    95
    val old_time: Time,
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    96
    val old_command_timings_blob: Bytes
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    97
  ) {
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77442
diff changeset
    98
    override def toString: String = name
77442
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
    99
  }
9969b6aed223 clarified modules (again);
wenzelm
parents: 77414
diff changeset
   100
77474
5ecaf881b563 clarified signature;
wenzelm
parents: 77473
diff changeset
   101
  class Session_Job private[Build_Job](
77455
ce53c1ce8536 tuned signature;
wenzelm
parents: 77454
diff changeset
   102
    build_context: Build_Process.Context,
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   103
    session_background: Sessions.Background,
77460
ccca589d7027 tuned signature: support general Build_Job instances;
wenzelm
parents: 77458
diff changeset
   104
    input_shasum: SHA1.Shasum,
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
   105
    override val node_info: Host.Node_Info
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   106
  ) extends Build_Job {
77455
ce53c1ce8536 tuned signature;
wenzelm
parents: 77454
diff changeset
   107
    private val store = build_context.store
ce53c1ce8536 tuned signature;
wenzelm
parents: 77454
diff changeset
   108
    private val progress = build_context.progress
ce53c1ce8536 tuned signature;
wenzelm
parents: 77454
diff changeset
   109
    private val verbose = build_context.verbose
ce53c1ce8536 tuned signature;
wenzelm
parents: 77454
diff changeset
   110
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   111
    def session_name: String = session_background.session_name
77349
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
   112
    def job_name: String = session_name
5a84de89170d more operations to support management of jobs, e.g. from external database;
wenzelm
parents: 77298
diff changeset
   113
77493
2d5529f56124 tuned signature;
wenzelm
parents: 77486
diff changeset
   114
    private val info: Sessions.Info = session_background.sessions_structure(session_name)
2d5529f56124 tuned signature;
wenzelm
parents: 77486
diff changeset
   115
    private val options: Options = Host.process_policy_options(info.options, node_info.numa_node)
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   116
77493
2d5529f56124 tuned signature;
wenzelm
parents: 77486
diff changeset
   117
    private val session_sources =
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   118
      Sessions.Sources.load(session_background.base, cache = store.cache.compress)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   119
77493
2d5529f56124 tuned signature;
wenzelm
parents: 77486
diff changeset
   120
    private val store_heap = build_context.store_heap(session_name)
77473
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   121
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   122
    private val future_result: Future[(Process_Result, SHA1.Shasum)] =
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   123
      Future.thread("build", uninterruptible = true) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   124
        val env =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   125
          Isabelle_System.settings(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   126
            List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   127
77473
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   128
        val session_heaps =
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   129
          session_background.info.parent match {
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   130
            case None => Nil
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   131
            case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   132
          }
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   133
77414
0d5994eef9e6 clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents: 77410
diff changeset
   134
        val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   135
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   136
        val eval_store =
77463
4e8bec105ce5 tuned signature;
wenzelm
parents: 77460
diff changeset
   137
          if (store_heap) {
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   138
            (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   139
            List("ML_Heap.save_child " +
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   140
              ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   141
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   142
          else Nil
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   143
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   144
        def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   145
          session_background.base.theory_load_commands.get(node_name.theory) match {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   146
            case None => Nil
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   147
            case Some(spans) =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   148
              val syntax = session_background.base.theory_syntax(node_name)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   149
              val master_dir = Path.explode(node_name.master_dir)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   150
              for (span <- spans; file <- span.loaded_files(syntax).files)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   151
                yield {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   152
                  val src_path = Path.explode(file)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   153
                  val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   154
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   155
                  val bytes = session_sources(blob_name.node).bytes
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   156
                  val text = bytes.text
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   157
                  val chunk = Symbol.Text_Chunk(text)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   158
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   159
                  Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) ->
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   160
                    Document.Blobs.Item(bytes, text, chunk, changed = false)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   161
                }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   162
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   163
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   164
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   165
        /* session */
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   166
77473
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   167
        val resources =
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   168
          new Resources(session_background, log = build_context.log,
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   169
            command_timings = build_context.old_command_timings(session_name))
362bf802013e clarified modules;
wenzelm
parents: 77465
diff changeset
   170
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   171
        val session =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   172
          new Session(options, resources) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   173
            override val cache: Term.Cache = store.cache
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   174
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   175
            override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   176
              Command.Blobs_Info.make(session_blobs(node_name))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   177
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   178
            override def build_blobs(node_name: Document.Node.Name): Document.Blobs =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   179
              Document.Blobs.make(session_blobs(node_name))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   180
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   181
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   182
        object Build_Session_Errors {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   183
          private val promise: Promise[List[String]] = Future.promise
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   184
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   185
          def result: Exn.Result[List[String]] = promise.join_result
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   186
          def cancel(): Unit = promise.cancel()
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   187
          def apply(errs: List[String]): Unit = {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   188
            try { promise.fulfill(errs) }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   189
            catch { case _: IllegalStateException => }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   190
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   191
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   192
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   193
        val export_consumer =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   194
          Export.consumer(store.open_database(session_name, output = true), store.cache,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   195
            progress = progress)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   196
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   197
        val stdout = new StringBuilder(1000)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   198
        val stderr = new StringBuilder(1000)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   199
        val command_timings = new mutable.ListBuffer[Properties.T]
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   200
        val theory_timings = new mutable.ListBuffer[Properties.T]
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   201
        val session_timings = new mutable.ListBuffer[Properties.T]
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   202
        val runtime_statistics = new mutable.ListBuffer[Properties.T]
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   203
        val task_statistics = new mutable.ListBuffer[Properties.T]
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   204
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   205
        def fun(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   206
          name: String,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   207
          acc: mutable.ListBuffer[Properties.T],
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   208
          unapply: Properties.T => Option[Properties.T]
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   209
        ): (String, Session.Protocol_Function) = {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   210
          name -> ((msg: Prover.Protocol_Output) =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   211
            unapply(msg.properties) match {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   212
              case Some(props) => acc += props; true
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   213
              case _ => false
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   214
            })
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   215
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   216
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   217
        session.init_protocol_handler(new Session.Protocol_Handler {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   218
            override def exit(): Unit = Build_Session_Errors.cancel()
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   219
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   220
            private def build_session_finished(msg: Prover.Protocol_Output): Boolean = {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   221
              val (rc, errors) =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   222
                try {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   223
                  val (rc, errs) = {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   224
                    import XML.Decode._
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   225
                    pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   226
                  }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   227
                  val errors =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   228
                    for (err <- errs) yield {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   229
                      val prt = Protocol_Message.expose_no_reports(err)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   230
                      Pretty.string_of(prt, metric = Symbol.Metric)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   231
                    }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   232
                  (rc, errors)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   233
                }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   234
                catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   235
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   236
              session.protocol_command("Prover.stop", rc.toString)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   237
              Build_Session_Errors(errors)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   238
              true
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   239
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   240
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   241
            private def loading_theory(msg: Prover.Protocol_Output): Boolean =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   242
              msg.properties match {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   243
                case Markup.Loading_Theory(Markup.Name(name)) =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   244
                  progress.theory(Progress.Theory(name, session = session_name))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   245
                  false
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   246
                case _ => false
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   247
              }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   248
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   249
            private def export_(msg: Prover.Protocol_Output): Boolean =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   250
              msg.properties match {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   251
                case Protocol.Export(args) =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   252
                  export_consumer.make_entry(session_name, args, msg.chunk)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   253
                  true
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   254
                case _ => false
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   255
              }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   256
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   257
            override val functions: Session.Protocol_Functions =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   258
              List(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   259
                Markup.Build_Session_Finished.name -> build_session_finished,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   260
                Markup.Loading_Theory.name -> loading_theory,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   261
                Markup.EXPORT -> export_,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   262
                fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   263
                fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   264
                fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   265
          })
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   266
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   267
        session.command_timings += Session.Consumer("command_timings") {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   268
          case Session.Command_Timing(props) =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   269
            for {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   270
              elapsed <- Markup.Elapsed.unapply(props)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   271
              elapsed_time = Time.seconds(elapsed)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   272
              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   273
            } command_timings += props.filter(Markup.command_timing_property)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   274
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   275
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   276
        session.runtime_statistics += Session.Consumer("ML_statistics") {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   277
          case Session.Runtime_Statistics(props) => runtime_statistics += props
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   278
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   279
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   280
        session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   281
          case snapshot =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   282
            if (!progress.stopped) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   283
              def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   284
                if (!progress.stopped) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   285
                  val theory_name = snapshot.node_name.theory
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   286
                  val args =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   287
                    Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   288
                  val body = Bytes(Symbol.encode(YXML.string_of_body(xml)))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   289
                  export_consumer.make_entry(session_name, args, body)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   290
                }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   291
              }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   292
              def export_text(name: String, text: String, compress: Boolean = true): Unit =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   293
                export_(name, List(XML.Text(text)), compress = compress)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   294
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   295
              for (command <- snapshot.snippet_command) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   296
                export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   297
              }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   298
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   299
              export_text(Export.FILES,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   300
                cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))),
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   301
                compress = false)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   302
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   303
              for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   304
                val xml = snapshot.switch(blob_name).xml_markup()
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   305
                export_(Export.MARKUP + (i + 1), xml)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   306
              }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   307
              export_(Export.MARKUP, snapshot.xml_markup())
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   308
              export_(Export.MESSAGES, snapshot.messages.map(_._1))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   309
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   310
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   311
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   312
        session.all_messages += Session.Consumer[Any]("build_session_output") {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   313
          case msg: Prover.Output =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   314
            val message = msg.message
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   315
            if (msg.is_system) resources.log(Protocol.message_text(message))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   316
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   317
            if (msg.is_stdout) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   318
              stdout ++= Symbol.encode(XML.content(message))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   319
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   320
            else if (msg.is_stderr) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   321
              stderr ++= Symbol.encode(XML.content(message))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   322
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   323
            else if (msg.is_exit) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   324
              val err =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   325
                "Prover terminated" +
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   326
                  (msg.properties match {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   327
                    case Markup.Process_Result(result) => ": " + result.print_rc
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   328
                    case _ => ""
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   329
                  })
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   330
              Build_Session_Errors(List(err))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   331
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   332
          case _ =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   333
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   334
77455
ce53c1ce8536 tuned signature;
wenzelm
parents: 77454
diff changeset
   335
        build_context.session_setup(session_name, session)
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   336
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   337
        val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   338
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   339
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   340
        /* process */
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   341
77485
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   342
        val process =
77414
0d5994eef9e6 clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents: 77410
diff changeset
   343
          Isabelle_Process.start(options, session, session_background, session_heaps,
0d5994eef9e6 clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents: 77410
diff changeset
   344
            use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env)
77485
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   345
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   346
        val timeout_request: Option[Event_Timer.Request] =
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   347
          if (info.timeout_ignored) None
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   348
          else Some(Event_Timer.request(Time.now() + info.timeout) { process.terminate() })
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   349
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   350
        val build_errors =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   351
          Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   352
            Exn.capture { process.await_startup() } match {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   353
              case Exn.Res(_) =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   354
                val resources_yxml = resources.init_session_yxml
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   355
                val encode_options: XML.Encode.T[Options] =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   356
                  options => session.prover_options(options).encode
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   357
                val args_yxml =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   358
                  YXML.string_of_body(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   359
                    {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   360
                      import XML.Encode._
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   361
                      pair(string, list(pair(encode_options, list(pair(string, properties)))))(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   362
                        (session_name, info.theories))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   363
                    })
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   364
                session.protocol_command("build_session", resources_yxml, args_yxml)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   365
                Build_Session_Errors.result
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   366
              case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   367
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   368
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   369
77484
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   370
        val result0 =
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   371
          Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   372
77485
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   373
        val was_timeout =
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   374
          timeout_request match {
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   375
            case None => false
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   376
            case Some(request) => !request.cancel()
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   377
          }
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   378
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   379
        session.stop()
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   380
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   381
        val export_errors =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   382
          export_consumer.shutdown(close = true).map(Output.error_message_text)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   383
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   384
        val (document_output, document_errors) =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   385
          try {
77484
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   386
            if (build_errors.isInstanceOf[Exn.Res[_]] && result0.ok && info.documents.nonEmpty) {
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   387
              using(Export.open_database_context(store)) { database_context =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   388
                val documents =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   389
                  using(database_context.open_session(session_background)) {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   390
                    session_context =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   391
                      Document_Build.build_documents(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   392
                        Document_Build.context(session_context, progress = progress),
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   393
                        output_sources = info.document_output,
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   394
                        output_pdf = info.document_output)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   395
                  }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   396
                using(database_context.open_database(session_name, output = true))(session_database =>
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   397
                  documents.foreach(_.write(session_database.db, session_name)))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   398
                (documents.flatMap(_.log_lines), Nil)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   399
              }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   400
            }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   401
            else (Nil, Nil)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   402
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   403
          catch {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   404
            case exn: Document_Build.Build_Error => (exn.log_lines, exn.log_errors)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   405
            case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   406
          }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   407
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   408
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   409
        /* process result */
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   410
77484
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   411
        val result1 = {
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   412
          val theory_timing =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   413
            theory_timings.iterator.flatMap(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   414
              {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   415
                case props @ Markup.Name(name) => Some(name -> props)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   416
                case _ => None
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   417
              }).toMap
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   418
          val used_theory_timings =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   419
            for { (name, _) <- session_background.base.used_theories }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   420
              yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   421
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   422
          val more_output =
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   423
            Library.trim_line(stdout.toString) ::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   424
              command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   425
              used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   426
              session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   427
              runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   428
              task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   429
              document_output
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   430
77484
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   431
          result0.output(more_output)
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   432
            .error(Library.trim_line(stderr.toString))
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   433
            .errors_rc(export_errors ::: document_errors)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   434
        }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   435
77484
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   436
        val result2 =
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   437
          build_errors match {
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   438
            case Exn.Res(build_errs) =>
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   439
              val errs = build_errs ::: document_errors
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   440
              if (errs.nonEmpty) {
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   441
                result1.error_rc.output(
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   442
                  errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   443
                    errs.map(Protocol.Error_Message_Marker.apply))
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   444
              }
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   445
              else if (progress.stopped && result1.ok) result1.copy(rc = Process_Result.RC.interrupt)
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   446
              else result1
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   447
            case Exn.Exn(Exn.Interrupt()) =>
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   448
              if (result1.ok) result1.copy(rc = Process_Result.RC.interrupt)
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   449
              else result1
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   450
            case Exn.Exn(exn) => throw exn
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   451
          }
7ba474a01249 tuned names;
wenzelm
parents: 77477
diff changeset
   452
77485
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   453
        val process_result =
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   454
          if (result2.ok) result2
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   455
          else if (was_timeout) result2.error(Output.error_message_text("Timeout")).timeout_rc
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   456
          else if (result2.interrupted) result2.error(Output.error_message_text("Interrupt"))
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   457
          else result2
911d3dbf2033 clarified timeout: closer to actual process;
wenzelm
parents: 77484
diff changeset
   458
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   459
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   460
        /* output heap */
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   461
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   462
        val output_shasum =
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   463
          if (process_result.ok && store_heap && store.output_heap(session_name).is_file) {
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   464
            SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   465
          }
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   466
          else SHA1.no_shasum
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   467
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   468
        val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   469
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   470
        val build_log =
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   471
          Build_Log.Log_File(session_name, process_result.out_lines).
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   472
            parse_session_info(
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   473
              command_timings = true,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   474
              theory_timings = true,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   475
              ml_statistics = true,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   476
              task_statistics = true)
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   477
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   478
        // write log file
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   479
        if (process_result.ok) {
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   480
          File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   481
        }
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   482
        else File.write(store.output_log(session_name), terminate_lines(log_lines))
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   483
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   484
        // write database
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   485
        using(store.open_database(session_name, output = true))(db =>
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   486
          store.write_session_info(db, session_name, session_sources,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   487
            build_log =
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   488
              if (process_result.timeout) build_log.error("Timeout") else build_log,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   489
            build =
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   490
              Sessions.Build_Info(
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   491
                sources = build_context.sources_shasum(session_name),
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   492
                input_heaps = input_shasum,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   493
                output_heap = output_shasum,
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   494
                process_result.rc, build_context.uuid)))
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   495
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   496
        // messages
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   497
        process_result.err_lines.foreach(progress.echo)
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   498
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   499
        if (process_result.ok) {
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   500
          if (verbose) {
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   501
            val props = build_log.session_timing
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   502
            val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   503
            val timing = Markup.Timing_Properties.get(props)
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   504
            progress.echo(
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   505
              "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")")
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   506
          }
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   507
          progress.echo(
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   508
            "Finished " + session_name + " (" + process_result.timing.message_resources + ")")
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   509
        }
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   510
        else {
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   511
          progress.echo(
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   512
            session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")")
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   513
          if (!process_result.interrupted) {
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   514
            val tail = info.options.int("process_output_tail")
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   515
            val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   516
            val prefix = if (log_lines.length == suffix.length) Nil else List("...")
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   517
            progress.echo(Library.trim_line(cat_lines(prefix ::: suffix)))
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   518
          }
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   519
        }
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   520
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   521
        (process_result.copy(out_lines = log_lines), output_shasum)
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   522
      }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   523
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   524
    override def cancel(): Unit = future_result.cancel()
77298
39c7d79ace34 clarified signature defaults;
wenzelm
parents: 77297
diff changeset
   525
    override def is_finished: Boolean = future_result.is_finished
77486
032c76e04475 clarified execution context: main work happens within Future.thread;
wenzelm
parents: 77485
diff changeset
   526
    override def join: (Process_Result, SHA1.Shasum) = future_result.join
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   527
  }
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77294
diff changeset
   528
77396
f184fbac99bc clarified modules;
wenzelm
parents: 77372
diff changeset
   529
75778
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   530
  /* theory markup/messages from session database */
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72853
diff changeset
   531
75778
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   532
  def read_theory(
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   533
    theory_context: Export.Theory_Context,
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   534
    unicode_symbols: Boolean = false
76205
005abcb34849 tuned signature;
wenzelm
parents: 76088
diff changeset
   535
  ): Option[Document.Snapshot] = {
76936
ee785742c694 proper treatment of unicode_symbols;
wenzelm
parents: 76935
diff changeset
   536
    def decode_bytes(bytes: Bytes): String =
ee785742c694 proper treatment of unicode_symbols;
wenzelm
parents: 76935
diff changeset
   537
      Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes))
ee785742c694 proper treatment of unicode_symbols;
wenzelm
parents: 76935
diff changeset
   538
75778
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   539
    def read(name: String): Export.Entry = theory_context(name, permissive = true)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   540
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   541
    def read_xml(name: String): XML.Body =
76936
ee785742c694 proper treatment of unicode_symbols;
wenzelm
parents: 76935
diff changeset
   542
      YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   543
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   544
    def read_source_file(name: String): Sessions.Source_File =
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   545
      theory_context.session_context.source_file(name)
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   546
75733
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   547
    for {
75778
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   548
      id <- theory_context.document_id()
75903
dce94a1d18fd proper permissive = true (amending 475fedc02737)
wenzelm
parents: 75791
diff changeset
   549
      (thy_file, blobs_files) <- theory_context.files(permissive = true)
75733
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   550
    }
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   551
    yield {
76881
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   552
      val master_dir =
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   553
        Path.explode(Url.strip_base_name(thy_file).getOrElse(
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   554
          error("Cannot determine theory master directory: " + quote(thy_file))))
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   555
75733
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   556
      val blobs =
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   557
        blobs_files.map { name =>
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   558
          val path = Path.explode(name)
76881
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   559
          val src_path = File.relative_path(master_dir, path).getOrElse(path)
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   560
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   561
          val file = read_source_file(name)
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   562
          val bytes = file.bytes
76936
ee785742c694 proper treatment of unicode_symbols;
wenzelm
parents: 76935
diff changeset
   563
          val text = decode_bytes(bytes)
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   564
          val chunk = Symbol.Text_Chunk(text)
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   565
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   566
          Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) ->
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   567
            Document.Blobs.Item(bytes, text, chunk, changed = false)
75733
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   568
        }
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   569
76936
ee785742c694 proper treatment of unicode_symbols;
wenzelm
parents: 76935
diff changeset
   570
      val thy_source = decode_bytes(read_source_file(thy_file).bytes)
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   571
      val thy_xml = read_xml(Export.MARKUP)
75733
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   572
      val blobs_xml =
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   573
        for (i <- (1 to blobs.length).toList)
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   574
          yield read_xml(Export.MARKUP + i)
72865
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
   575
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   576
      val markups_index = Command.Markup_Index.make(blobs.map(_._1))
75733
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   577
      val markups =
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   578
        Command.Markups.make(
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   579
          for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   580
          yield index -> Markup_Tree.from_XML(xml))
d3430f302c2e clarified signature;
wenzelm
parents: 75454
diff changeset
   581
76911
wenzelm
parents: 76908
diff changeset
   582
      val results =
wenzelm
parents: 76908
diff changeset
   583
        Command.Results.make(
wenzelm
parents: 76908
diff changeset
   584
          for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
wenzelm
parents: 76908
diff changeset
   585
            yield i -> elem)
wenzelm
parents: 76908
diff changeset
   586
76205
005abcb34849 tuned signature;
wenzelm
parents: 76088
diff changeset
   587
      val command =
76881
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   588
        Command.unparsed(thy_source, theory = true, id = id,
b59118d11a46 clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm
parents: 76879
diff changeset
   589
          node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
76913
a8eb5046b05f tuned signature;
wenzelm
parents: 76912
diff changeset
   590
          blobs_info = Command.Blobs_Info.make(blobs),
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   591
          markups = markups, results = results)
76205
005abcb34849 tuned signature;
wenzelm
parents: 76088
diff changeset
   592
76913
a8eb5046b05f tuned signature;
wenzelm
parents: 76912
diff changeset
   593
      val doc_blobs = Document.Blobs.make(blobs)
76912
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   594
ca872f20cf5b clarified session sources: theory and blobs are read from database, instead of physical file-system;
wenzelm
parents: 76911
diff changeset
   595
      Document.State.init.snippet(command, doc_blobs)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   596
    }
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   597
  }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   598
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   599
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   600
  /* print messages */
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   601
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   602
  def print_log(
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   603
    options: Options,
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   604
    sessions: List[String],
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   605
    theories: List[String] = Nil,
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   606
    message_head: List[Regex] = Nil,
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   607
    message_body: List[Regex] = Nil,
72878
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   608
    verbose: Boolean = false,
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   609
    progress: Progress = new Progress,
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   610
    margin: Double = Pretty.default_margin,
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   611
    breakgain: Double = Pretty.default_breakgain,
72873
0ad513706a27 clarified Pretty.Metric, as for build errors;
wenzelm
parents: 72871
diff changeset
   612
    metric: Pretty.Metric = Symbol.Metric,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74755
diff changeset
   613
    unicode_symbols: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74755
diff changeset
   614
  ): Unit = {
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   615
    val store = Sessions.store(options)
76654
a3177042863d tuned signature;
wenzelm
parents: 76205
diff changeset
   616
    val session = new Session(options, Resources.bootstrap)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   617
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   618
    def check(filter: List[Regex], make_string: => String): Boolean =
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   619
      filter.isEmpty || {
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   620
        val s = Output.clean_yxml(make_string)
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   621
        filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty)
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   622
      }
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   623
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   624
    def print(session_name: String): Unit = {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   625
      using(Export.open_session_context0(store, session_name)) { session_context =>
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   626
        val result =
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   627
          for {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   628
            db <- session_context.session_db()
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   629
            theories = store.read_theories(db, session_name)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   630
            errors = store.read_errors(db, session_name)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   631
            info <- store.read_build(db, session_name)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   632
          } yield (theories, errors, info.return_code)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   633
        result match {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   634
          case None => store.error_database(session_name)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   635
          case Some((used_theories, errors, rc)) =>
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   636
            theories.filterNot(used_theories.toSet) match {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   637
              case Nil =>
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   638
              case bad => error("Unknown theories " + commas_quote(bad))
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   639
            }
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   640
            val print_theories =
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   641
              if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
75778
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   642
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   643
            for (thy <- print_theories) {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   644
              val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":"
75778
d18c96b9b955 prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;
wenzelm
parents: 75762
diff changeset
   645
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   646
              read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   647
                case None => progress.echo(thy_heading + " MISSING")
76205
005abcb34849 tuned signature;
wenzelm
parents: 76088
diff changeset
   648
                case Some(snapshot) =>
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   649
                  val rendering = new Rendering(snapshot, options, session)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   650
                  val messages =
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   651
                    rendering.text_messages(Text.Range.full)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   652
                      .filter(message => verbose || Protocol.is_exported(message.info))
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   653
                  if (messages.nonEmpty) {
76933
dd53bb198eb1 tuned signature: more uniform operations;
wenzelm
parents: 76930
diff changeset
   654
                    val line_document = Line.Document(snapshot.node.source)
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   655
                    val buffer = new mutable.ListBuffer[String]
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   656
                    for (Text.Info(range, elem) <- messages) {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   657
                      val line = line_document.position(range.start).line1
76205
005abcb34849 tuned signature;
wenzelm
parents: 76088
diff changeset
   658
                      val pos = Position.Line_File(line, snapshot.node_name.node)
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   659
                      def message_text: String =
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   660
                        Protocol.message_text(elem, heading = true, pos = pos,
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   661
                          margin = margin, breakgain = breakgain, metric = metric)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   662
                      val ok =
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   663
                        check(message_head, Protocol.message_heading(elem, pos)) &&
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   664
                        check(message_body, XML.content(Pretty.unformatted(List(elem))))
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   665
                      if (ok) buffer += message_text
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   666
                    }
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   667
                    if (buffer.nonEmpty) {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   668
                      progress.echo(thy_heading)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   669
                      buffer.foreach(progress.echo)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   670
                    }
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   671
                  }
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   672
              }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   673
            }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   674
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   675
            if (errors.nonEmpty) {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   676
              val msg = Symbol.output(unicode_symbols, cat_lines(errors))
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   677
              progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   678
            }
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   679
            if (rc != Process_Result.RC.ok) {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   680
              progress.echo("\n" + Process_Result.RC.print_long(rc))
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   681
            }
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   682
        }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   683
      }
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   684
    }
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   685
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   686
    val errors = new mutable.ListBuffer[String]
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   687
    for (session_name <- sessions) {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   688
      Exn.interruptible_capture(print(session_name)) match {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   689
        case Exn.Res(_) =>
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   690
        case Exn.Exn(exn) => errors += Exn.message(exn)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   691
      }
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   692
    }
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   693
    if (errors.nonEmpty) error(cat_lines(errors.toList))
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   694
  }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   695
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   696
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   697
  /* Isabelle tool wrapper */
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   698
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   699
  val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   700
    Scala_Project.here,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   701
    { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   702
      /* arguments */
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   703
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   704
      var message_head = List.empty[Regex]
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   705
      var message_body = List.empty[Regex]
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   706
      var unicode_symbols = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   707
      var theories: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   708
      var margin = Pretty.default_margin
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   709
      var options = Options.init()
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   710
      var verbose = false
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   711
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   712
      val getopts = Getopts("""
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   713
Usage: isabelle log [OPTIONS] [SESSIONS ...]
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   714
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   715
  Options are:
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   716
    -H REGEX     filter messages by matching against head
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   717
    -M REGEX     filter messages by matching against body
72876
626fcaebd049 NEWS and documentation for "isabelle log";
wenzelm
parents: 72875
diff changeset
   718
    -T NAME      restrict to given theories (multiple options possible)
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
   719
    -U           output Unicode symbols
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   720
    -m MARGIN    margin for pretty printing (default: """ + margin + """)
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   721
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
73837
f72335f6a9ed clarified documentation: tracing messages are not shown here;
wenzelm
parents: 73835
diff changeset
   722
    -v           print all messages, including information etc.
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   723
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   724
  Print messages from the build database of the given sessions, without any
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   725
  checks against current sources nor session structure: results from old
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   726
  sessions or failed builds can be printed as well.
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   727
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   728
  Multiple options -H and -M are conjunctive: all given patterns need to
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   729
  match. Patterns match any substring, but ^ or $ may be used to match the
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   730
  start or end explicitly.
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   731
""",
76087
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   732
        "H:" -> (arg => message_head = message_head ::: List(arg.r)),
c8f5fec36b5c support regex patterns on messages;
wenzelm
parents: 75970
diff changeset
   733
        "M:" -> (arg => message_body = message_body ::: List(arg.r)),
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   734
        "T:" -> (arg => theories = theories ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   735
        "U" -> (_ => unicode_symbols = true),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   736
        "m:" -> (arg => margin = Value.Double.parse(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   737
        "o:" -> (arg => options = options + arg),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   738
        "v" -> (_ => verbose = true))
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   739
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   740
      val sessions = getopts(args)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   741
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   742
      val progress = new Console_Progress()
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   743
76088
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   744
      if (sessions.isEmpty) progress.echo_warning("No sessions to print")
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   745
      else {
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   746
        print_log(options, sessions, theories = theories, message_head = message_head,
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   747
          message_body = message_body, verbose = verbose, margin = margin, progress = progress,
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   748
          unicode_symbols = unicode_symbols)
bec8677d0e5b support multiple sessions, with cumulative errors;
wenzelm
parents: 76087
diff changeset
   749
      }
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   750
    })
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   751
}