src/Pure/Tools/build_job.scala
author wenzelm
Thu, 11 Nov 2021 21:54:28 +0100
changeset 74755 510296c0d8d1
parent 74731 161e84e6b40a
child 75393 87ebf5a50283
permissions -rw-r--r--
clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
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
73897
0ddb5de0506e clarified signature: prefer Java interfaces;
wenzelm
parents: 73837
diff changeset
    10
import java.util.HashMap
0ddb5de0506e clarified signature: prefer Java interfaces;
wenzelm
parents: 73837
diff changeset
    11
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    12
import scala.collection.mutable
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    13
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
    14
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    15
object Build_Job
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    16
{
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72853
diff changeset
    17
  /* theory markup/messages from database */
6c660f05f70c clarified signature;
wenzelm
parents: 72853
diff changeset
    18
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    19
  def read_theory(
72857
a9e091ccd450 clarified signature;
wenzelm
parents: 72856
diff changeset
    20
    db_context: Sessions.Database_Context,
74712
bcca7e3bcd0d proper treatment of session build hierarchy;
wenzelm
parents: 74685
diff changeset
    21
    session_hierarchy: List[String],
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
    22
    theory: String,
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
    23
    unicode_symbols: Boolean = false): Option[Command] =
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    24
  {
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    25
    def read(name: String): Export.Entry =
74712
bcca7e3bcd0d proper treatment of session build hierarchy;
wenzelm
parents: 74685
diff changeset
    26
      db_context.get_export(session_hierarchy, theory, name)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    27
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    28
    def read_xml(name: String): XML.Body =
73033
d2690444c00a clarified caching;
wenzelm
parents: 73031
diff changeset
    29
      YXML.parse_body(
d2690444c00a clarified caching;
wenzelm
parents: 73031
diff changeset
    30
        Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
d2690444c00a clarified caching;
wenzelm
parents: 73031
diff changeset
    31
        cache = db_context.cache)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    32
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    33
    (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    34
      case (Value.Long(id), thy_file :: blobs_files) =>
74755
510296c0d8d1 clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents: 74731
diff changeset
    35
        val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    36
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    37
        val results =
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    38
          Command.Results.make(
72871
wenzelm
parents: 72869
diff changeset
    39
            for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
wenzelm
parents: 72869
diff changeset
    40
              yield i -> elem)
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    41
72865
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    42
        val blobs =
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    43
          blobs_files.map(file =>
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    44
          {
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    45
            val path = Path.explode(file)
74755
510296c0d8d1 clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents: 74731
diff changeset
    46
            val name = Resources.file_node(path)
72964
2621225b4bdd proper relative path;
wenzelm
parents: 72962
diff changeset
    47
            val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
72865
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    48
            Command.Blob(name, src_path, None)
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    49
          })
72864
wenzelm
parents: 72863
diff changeset
    50
        val blobs_xml =
wenzelm
parents: 72863
diff changeset
    51
          for (i <- (1 to blobs.length).toList)
72865
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    52
            yield read_xml(Export.MARKUP + i)
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    53
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    54
        val blobs_info =
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    55
          Command.Blobs_Info(
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    56
            for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    57
              yield {
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    58
                val text = XML.content(xml)
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    59
                val chunk = Symbol.Text_Chunk(text)
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    60
                val digest = SHA1.digest(Symbol.encode(text))
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    61
                Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    62
              })
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    63
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    64
        val thy_xml = read_xml(Export.MARKUP)
ebf72a3b8daa clarified file sources: take from build database instead of file-system;
wenzelm
parents: 72864
diff changeset
    65
        val thy_source = XML.content(thy_xml)
72864
wenzelm
parents: 72863
diff changeset
    66
wenzelm
parents: 72863
diff changeset
    67
        val markups_index =
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    68
          Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    69
        val markups =
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    70
          Command.Markups.make(
72864
wenzelm
parents: 72863
diff changeset
    71
            for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
wenzelm
parents: 72863
diff changeset
    72
            yield index -> Markup_Tree.from_XML(xml))
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    73
72853
d0038b553e0e clarified signature: name according to db model without Sessions.Structure/Deps;
wenzelm
parents: 72849
diff changeset
    74
        val command =
d0038b553e0e clarified signature: name according to db model without Sessions.Structure/Deps;
wenzelm
parents: 72849
diff changeset
    75
          Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
d0038b553e0e clarified signature: name according to db model without Sessions.Structure/Deps;
wenzelm
parents: 72849
diff changeset
    76
            blobs_info = blobs_info, results = results, markups = markups)
d0038b553e0e clarified signature: name according to db model without Sessions.Structure/Deps;
wenzelm
parents: 72849
diff changeset
    77
        Some(command)
d0038b553e0e clarified signature: name according to db model without Sessions.Structure/Deps;
wenzelm
parents: 72849
diff changeset
    78
      case _ => None
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    79
    }
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
    80
  }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    81
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    82
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    83
  /* print messages */
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    84
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    85
  def print_log(
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    86
    options: Options,
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    87
    session_name: String,
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    88
    theories: List[String] = Nil,
72878
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
    89
    verbose: Boolean = false,
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    90
    progress: Progress = new Progress,
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    91
    margin: Double = Pretty.default_margin,
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    92
    breakgain: Double = Pretty.default_breakgain,
72873
0ad513706a27 clarified Pretty.Metric, as for build errors;
wenzelm
parents: 72871
diff changeset
    93
    metric: Pretty.Metric = Symbol.Metric,
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73134
diff changeset
    94
    unicode_symbols: Boolean = false): Unit =
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    95
  {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    96
    val store = Sessions.store(options)
74755
510296c0d8d1 clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents: 74731
diff changeset
    97
    val session = new Session(options, Resources.empty)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    98
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
    99
    using(store.open_database_context())(db_context =>
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   100
    {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   101
      val result =
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   102
        db_context.input_database(session_name)((db, _) =>
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   103
        {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   104
          val theories = store.read_theories(db, session_name)
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   105
          val errors = store.read_errors(db, session_name)
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   106
          store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   107
        })
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   108
      result match {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   109
        case None => error("Missing build database for session " + quote(session_name))
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   110
        case Some((used_theories, errors, rc)) =>
73835
5dae03d50db1 more formal ML profiling messages;
wenzelm
parents: 73805
diff changeset
   111
          theories.filterNot(used_theories.toSet) match {
5dae03d50db1 more formal ML profiling messages;
wenzelm
parents: 73805
diff changeset
   112
            case Nil =>
5dae03d50db1 more formal ML profiling messages;
wenzelm
parents: 73805
diff changeset
   113
            case bad => error("Unknown theories " + commas_quote(bad))
5dae03d50db1 more formal ML profiling messages;
wenzelm
parents: 73805
diff changeset
   114
          }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   115
          val print_theories =
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   116
            if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   117
          for (thy <- print_theories) {
72868
90e28f005be9 tuned messages;
wenzelm
parents: 72867
diff changeset
   118
            val thy_heading = "\nTheory " + quote(thy) + ":"
74755
510296c0d8d1 clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents: 74731
diff changeset
   119
            read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols)
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
   120
            match {
72863
a261946dafa3 tuned messages;
wenzelm
parents: 72859
diff changeset
   121
              case None => progress.echo(thy_heading + " MISSING")
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   122
              case Some(command) =>
72958
0d8bc0252e2e tuned signature;
wenzelm
parents: 72882
diff changeset
   123
                val snapshot = Document.State.init.snippet(command)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   124
                val rendering = new Rendering(snapshot, options, session)
72878
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   125
                val messages =
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   126
                  rendering.text_messages(Text.Range.full)
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   127
                    .filter(message => verbose || Protocol.is_exported(message.info))
72863
a261946dafa3 tuned messages;
wenzelm
parents: 72859
diff changeset
   128
                if (messages.nonEmpty) {
72875
847c6fb05a21 clarified messages;
wenzelm
parents: 72874
diff changeset
   129
                  val line_document = Line.Document(command.source)
72863
a261946dafa3 tuned messages;
wenzelm
parents: 72859
diff changeset
   130
                  progress.echo(thy_heading)
72875
847c6fb05a21 clarified messages;
wenzelm
parents: 72874
diff changeset
   131
                  for (Text.Info(range, elem) <- messages) {
847c6fb05a21 clarified messages;
wenzelm
parents: 72874
diff changeset
   132
                    val line = line_document.position(range.start).line1
847c6fb05a21 clarified messages;
wenzelm
parents: 72874
diff changeset
   133
                    val pos = Position.Line_File(line, command.node_name.node)
72863
a261946dafa3 tuned messages;
wenzelm
parents: 72859
diff changeset
   134
                    progress.echo(
72875
847c6fb05a21 clarified messages;
wenzelm
parents: 72874
diff changeset
   135
                      Protocol.message_text(elem, heading = true, pos = pos,
847c6fb05a21 clarified messages;
wenzelm
parents: 72874
diff changeset
   136
                        margin = margin, breakgain = breakgain, metric = metric))
72863
a261946dafa3 tuned messages;
wenzelm
parents: 72859
diff changeset
   137
                  }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   138
                }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   139
            }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   140
          }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   141
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   142
          if (errors.nonEmpty) {
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
   143
            val msg = Symbol.output(unicode_symbols, cat_lines(errors))
72868
90e28f005be9 tuned messages;
wenzelm
parents: 72867
diff changeset
   144
            progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   145
          }
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74259
diff changeset
   146
          if (rc != Process_Result.RC.ok) {
a117c076aa22 clarified signature;
wenzelm
parents: 74259
diff changeset
   147
            progress.echo("\n" + Process_Result.RC.print_long(rc))
a117c076aa22 clarified signature;
wenzelm
parents: 74259
diff changeset
   148
          }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   149
      }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   150
    })
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   151
  }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   152
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   153
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   154
  /* Isabelle tool wrapper */
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   155
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   156
  val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   157
    Scala_Project.here, args =>
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   158
  {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   159
    /* arguments */
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   160
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
   161
    var unicode_symbols = false
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   162
    var theories: List[String] = Nil
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   163
    var margin = Pretty.default_margin
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   164
    var options = Options.init()
72878
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   165
    var verbose = false
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   166
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   167
    val getopts = Getopts("""
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   168
Usage: isabelle log [OPTIONS] SESSION
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   169
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   170
  Options are:
72876
626fcaebd049 NEWS and documentation for "isabelle log";
wenzelm
parents: 72875
diff changeset
   171
    -T NAME      restrict to given theories (multiple options possible)
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
   172
    -U           output Unicode symbols
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   173
    -m MARGIN    margin for pretty printing (default: """ + margin + """)
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   174
    -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
   175
    -v           print all messages, including information etc.
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   176
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   177
  Print messages from the build database of the given session, without any
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   178
  checks against current sources: results from a failed build can be
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   179
  printed as well.
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   180
""",
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   181
      "T:" -> (arg => theories = theories ::: List(arg)),
72867
7b10b40b1273 clarified output of Isabelle symbols;
wenzelm
parents: 72865
diff changeset
   182
      "U" -> (_ => unicode_symbols = true),
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   183
      "m:" -> (arg => margin = Value.Double.parse(arg)),
72878
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   184
      "o:" -> (arg => options = options + arg),
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   185
      "v" -> (_ => verbose = true))
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   186
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   187
    val more_args = getopts(args)
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   188
    val session_name =
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   189
      more_args match {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   190
        case List(session_name) => session_name
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   191
        case _ => getopts.usage()
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   192
      }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   193
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   194
    val progress = new Console_Progress()
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   195
72878
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   196
    print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
80465b791f95 clarified messages;
wenzelm
parents: 72876
diff changeset
   197
      progress = progress, unicode_symbols = unicode_symbols)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72857
diff changeset
   198
  })
72848
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   199
}
d5d0e36eda16 read theory with PIDE markup from session database;
wenzelm
parents: 72844
diff changeset
   200
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   201
class Build_Job(progress: Progress,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   202
  session_name: String,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   203
  val info: Sessions.Info,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   204
  deps: Sessions.Deps,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   205
  store: Sessions.Store,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   206
  do_store: Boolean,
73777
52e43a93d51f clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents: 73774
diff changeset
   207
  log: Logger,
73805
b73777a0c076 allow build session setup, e.g. for protocol handlers;
wenzelm
parents: 73804
diff changeset
   208
  session_setup: (String, Session) => Unit,
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   209
  val numa_node: Option[Int],
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   210
  command_timings0: List[Properties.T])
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   211
{
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   212
  val options: Options = NUMA.policy_options(info.options, numa_node)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   213
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   214
  private val sessions_structure = deps.sessions_structure
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   215
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   216
  private val future_result: Future[Process_Result] =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   217
    Future.thread("build", uninterruptible = true) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   218
      val parent = info.parent.getOrElse("")
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   219
      val base = deps(parent)
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   220
      val result_base = deps(session_name)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   221
73897
0ddb5de0506e clarified signature: prefer Java interfaces;
wenzelm
parents: 73837
diff changeset
   222
      val env = new HashMap(Isabelle_System.settings())
0ddb5de0506e clarified signature: prefer Java interfaces;
wenzelm
parents: 73837
diff changeset
   223
      env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   224
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   225
      val is_pure = Sessions.is_pure(session_name)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   226
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   227
      val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   228
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   229
      val eval_store =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   230
        if (do_store) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   231
          (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   232
          List("ML_Heap.save_child " +
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   233
            ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   234
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   235
        else Nil
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   236
73774
734d5d3fbd9d syslog option for "isabelle build";
wenzelm
parents: 73719
diff changeset
   237
      val resources =
734d5d3fbd9d syslog option for "isabelle build";
wenzelm
parents: 73719
diff changeset
   238
        new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   239
      val session =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   240
        new Session(options, resources) {
74731
161e84e6b40a just one cache, via HTML_Context, via Sessions.Store or Session;
wenzelm
parents: 74712
diff changeset
   241
          override val cache: Term.Cache = store.cache
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   242
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   243
          override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   244
          {
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   245
            result_base.load_commands.get(name.expand) match {
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   246
              case Some(spans) =>
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   247
                val syntax = result_base.theory_syntax(name)
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   248
                Command.build_blobs_info(syntax, name, spans)
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   249
              case None => Command.Blobs_Info.none
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   250
            }
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   251
          }
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   252
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   253
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   254
      object Build_Session_Errors
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   255
      {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   256
        private val promise: Promise[List[String]] = Future.promise
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   257
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   258
        def result: Exn.Result[List[String]] = promise.join_result
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   259
        def cancel(): Unit = promise.cancel()
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73134
diff changeset
   260
        def apply(errs: List[String]): Unit =
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   261
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   262
          try { promise.fulfill(errs) }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   263
          catch { case _: IllegalStateException => }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   264
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   265
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   266
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   267
      val export_consumer =
74255
e117e0c29204 more reactive interrupt;
wenzelm
parents: 74144
diff changeset
   268
        Export.consumer(store.open_database(session_name, output = true), store.cache,
e117e0c29204 more reactive interrupt;
wenzelm
parents: 74144
diff changeset
   269
          progress = progress)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   270
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   271
      val stdout = new StringBuilder(1000)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   272
      val stderr = new StringBuilder(1000)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   273
      val command_timings = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   274
      val theory_timings = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   275
      val session_timings = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   276
      val runtime_statistics = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   277
      val task_statistics = new mutable.ListBuffer[Properties.T]
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   278
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   279
      def fun(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   280
        name: String,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   281
        acc: mutable.ListBuffer[Properties.T],
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   282
        unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   283
      {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   284
        name -> ((msg: Prover.Protocol_Output) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   285
          unapply(msg.properties) match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   286
            case Some(props) => acc += props; true
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   287
            case _ => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   288
          })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   289
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   290
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   291
      session.init_protocol_handler(new Session.Protocol_Handler
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   292
        {
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   293
          override def exit(): Unit = Build_Session_Errors.cancel()
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   294
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   295
          private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   296
          {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   297
            val (rc, errors) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   298
              try {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   299
                val (rc, errs) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   300
                {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   301
                  import XML.Decode._
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   302
                  pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   303
                }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   304
                val errors =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   305
                  for (err <- errs) yield {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   306
                    val prt = Protocol_Message.expose_no_reports(err)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   307
                    Pretty.string_of(prt, metric = Symbol.Metric)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   308
                  }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   309
                (rc, errors)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   310
              }
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74259
diff changeset
   311
              catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   312
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   313
            session.protocol_command("Prover.stop", rc.toString)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   314
            Build_Session_Errors(errors)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   315
            true
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   316
          }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   317
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   318
          private def loading_theory(msg: Prover.Protocol_Output): Boolean =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   319
            msg.properties match {
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   320
              case Markup.Loading_Theory(Markup.Name(name)) =>
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   321
                progress.theory(Progress.Theory(name, session = session_name))
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   322
                false
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   323
              case _ => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   324
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   325
74685
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   326
          private def export_(msg: Prover.Protocol_Output): Boolean =
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   327
            msg.properties match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   328
              case Protocol.Export(args) =>
73559
22b5ecb53dd9 more uniform use of Byte_Message;
wenzelm
parents: 73367
diff changeset
   329
                export_consumer(session_name, args, msg.chunk)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   330
                true
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   331
              case _ => false
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   332
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   333
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   334
          override val functions =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   335
            List(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   336
              Markup.Build_Session_Finished.name -> build_session_finished,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   337
              Markup.Loading_Theory.name -> loading_theory,
74685
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   338
              Markup.EXPORT -> export_,
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   339
              fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   340
              fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   341
              fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   342
        })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   343
72711
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   344
      session.command_timings += Session.Consumer("command_timings")
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   345
        {
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   346
          case Session.Command_Timing(props) =>
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   347
            for {
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   348
              elapsed <- Markup.Elapsed.unapply(props)
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   349
              elapsed_time = Time.seconds(elapsed)
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   350
              if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   351
            } command_timings += props.filter(Markup.command_timing_property)
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   352
        }
9e89c2e15d36 clarified command_timings protocol;
wenzelm
parents: 72701
diff changeset
   353
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   354
      session.runtime_statistics += Session.Consumer("ML_statistics")
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   355
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   356
          case Session.Runtime_Statistics(props) => runtime_statistics += props
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   357
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   358
72721
79f5e843e5ec clarified signature: prefer high-level Snapshot over low-level Command.State;
wenzelm
parents: 72717
diff changeset
   359
      session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   360
        {
72721
79f5e843e5ec clarified signature: prefer high-level Snapshot over low-level Command.State;
wenzelm
parents: 72717
diff changeset
   361
          case snapshot =>
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   362
            if (!progress.stopped) {
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   363
              val rendering = new Rendering(snapshot, options, session)
72730
01c9b3033036 more exports from rendering;
wenzelm
parents: 72726
diff changeset
   364
74685
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   365
              def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit =
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   366
              {
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   367
                if (!progress.stopped) {
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   368
                  val theory_name = snapshot.node_name.theory
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   369
                  val args =
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   370
                    Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   371
                  val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml)))
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   372
                  if (!bytes.is_empty) export_consumer(session_name, args, bytes)
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   373
                }
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   374
              }
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   375
              def export_text(name: String, text: String, compress: Boolean = true): Unit =
74685
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   376
                export_(name, List(XML.Text(text)), compress = compress)
72730
01c9b3033036 more exports from rendering;
wenzelm
parents: 72726
diff changeset
   377
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   378
              for (command <- snapshot.snippet_command) {
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   379
                export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   380
              }
72844
240c8a0f6337 clarified exports;
wenzelm
parents: 72817
diff changeset
   381
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   382
              export_text(Export.FILES,
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   383
                cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72783
diff changeset
   384
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   385
              for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
74685
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   386
                export_(Export.MARKUP + (i + 1), xml)
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   387
              }
74685
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   388
              export_(Export.MARKUP, snapshot.xml_markup())
0ab5e35ac964 avoid conflict with future keyword;
wenzelm
parents: 74657
diff changeset
   389
              export_(Export.MESSAGES, snapshot.messages.map(_._1))
74258
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   390
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   391
              val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
e942eedd9229 more reactive interrupt;
wenzelm
parents: 74255
diff changeset
   392
              export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations))
72817
1c378ab75d48 clarified signature, notably access to blob files;
wenzelm
parents: 72816
diff changeset
   393
            }
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   394
        }
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 72683
diff changeset
   395
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   396
      session.all_messages += Session.Consumer[Any]("build_session_output")
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   397
        {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   398
          case msg: Prover.Output =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   399
            val message = msg.message
73777
52e43a93d51f clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents: 73774
diff changeset
   400
            if (msg.is_system) resources.log(Protocol.message_text(message))
73774
734d5d3fbd9d syslog option for "isabelle build";
wenzelm
parents: 73719
diff changeset
   401
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   402
            if (msg.is_stdout) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   403
              stdout ++= Symbol.encode(XML.content(message))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   404
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   405
            else if (msg.is_stderr) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   406
              stderr ++= Symbol.encode(XML.content(message))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   407
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   408
            else if (msg.is_exit) {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   409
              val err =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   410
                "Prover terminated" +
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   411
                  (msg.properties match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   412
                    case Markup.Process_Result(result) => ": " + result.print_rc
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   413
                    case _ => ""
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   414
                  })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   415
              Build_Session_Errors(List(err))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   416
            }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   417
          case _ =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   418
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   419
73805
b73777a0c076 allow build session setup, e.g. for protocol handlers;
wenzelm
parents: 73804
diff changeset
   420
      session_setup(session_name, session)
b73777a0c076 allow build session setup, e.g. for protocol handlers;
wenzelm
parents: 73804
diff changeset
   421
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   422
      val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   423
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   424
      val process =
73802
8d9ac6cfc270 clarified signature;
wenzelm
parents: 73785
diff changeset
   425
        Isabelle_Process.start(session, options, sessions_structure, store,
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   426
          logic = parent, raw_ml_system = is_pure,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   427
          use_prelude = use_prelude, eval_main = eval_main,
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   428
          cwd = info.dir.file, env = env)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   429
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   430
      val build_errors =
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   431
        Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   432
          Exn.capture { process.await_startup() } match {
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   433
            case Exn.Res(_) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   434
              val resources_yxml = resources.init_session_yxml
74144
f9f6a31cc99c proper prover_options for batch-build;
wenzelm
parents: 74067
diff changeset
   435
              val encode_options: XML.Encode.T[Options] =
f9f6a31cc99c proper prover_options for batch-build;
wenzelm
parents: 74067
diff changeset
   436
                options => session.prover_options(options).encode
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   437
              val args_yxml =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   438
                YXML.string_of_body(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   439
                  {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   440
                    import XML.Encode._
74144
f9f6a31cc99c proper prover_options for batch-build;
wenzelm
parents: 74067
diff changeset
   441
                    pair(string, list(pair(encode_options, list(pair(string, properties)))))(
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   442
                      (session_name, info.theories))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   443
                  })
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   444
              session.protocol_command("build_session", resources_yxml, args_yxml)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   445
              Build_Session_Errors.result
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   446
            case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   447
          }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   448
        }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   449
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   450
      val process_result =
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   451
        Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   452
72697
e16f85e3c288 more robust;
wenzelm
parents: 72696
diff changeset
   453
      session.stop()
e16f85e3c288 more robust;
wenzelm
parents: 72696
diff changeset
   454
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   455
      val export_errors =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   456
        export_consumer.shutdown(close = true).map(Output.error_message_text)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   457
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72697
diff changeset
   458
      val (document_output, document_errors) =
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   459
        try {
72881
220a094a42d8 proper else statement;
wenzelm
parents: 72879
diff changeset
   460
          if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72853
diff changeset
   461
            using(store.open_database_context())(db_context =>
72715
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   462
              {
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   463
                val documents =
73719
d4c7b88f56a0 misc tuning and clarification;
wenzelm
parents: 73718
diff changeset
   464
                  Document_Build.build_documents(
d4c7b88f56a0 misc tuning and clarification;
wenzelm
parents: 73718
diff changeset
   465
                    Document_Build.context(session_name, deps, db_context, progress = progress),
72715
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   466
                    output_sources = info.document_output,
73781
0909fd14f8a4 avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;
wenzelm
parents: 73777
diff changeset
   467
                    output_pdf = info.document_output)
72715
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   468
                db_context.output_database(session_name)(db =>
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   469
                  documents.foreach(_.write(db, session_name)))
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   470
                (documents.flatMap(_.log_lines), Nil)
2615b8c05337 clarified signature --- avoid repeated open_database on server;
wenzelm
parents: 72711
diff changeset
   471
              })
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   472
          }
72881
220a094a42d8 proper else statement;
wenzelm
parents: 72879
diff changeset
   473
          else (Nil, Nil)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   474
        }
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72881
diff changeset
   475
        catch {
73718
ecb31c3bf980 clarified modules;
wenzelm
parents: 73700
diff changeset
   476
          case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72881
diff changeset
   477
          case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
1dc2ad97e062 more informative error;
wenzelm
parents: 72881
diff changeset
   478
        }
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   479
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   480
      val result =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   481
      {
72738
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   482
        val theory_timing =
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   483
          theory_timings.iterator.map(
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   484
            { case props @ Markup.Name(name) => name -> props }).toMap
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   485
        val used_theory_timings =
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   486
          for { (name, _) <- deps(session_name).used_theories }
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   487
            yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   488
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   489
        val more_output =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   490
          Library.trim_line(stdout.toString) ::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   491
            command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
72738
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72730
diff changeset
   492
            used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   493
            session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   494
            runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   495
            task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72697
diff changeset
   496
            document_output
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   497
72726
ec6a27bbdab8 proper return code for more errors (amending d892f6d66402);
wenzelm
parents: 72725
diff changeset
   498
        process_result.output(more_output)
ec6a27bbdab8 proper return code for more errors (amending d892f6d66402);
wenzelm
parents: 72725
diff changeset
   499
          .error(Library.trim_line(stderr.toString))
ec6a27bbdab8 proper return code for more errors (amending d892f6d66402);
wenzelm
parents: 72725
diff changeset
   500
          .errors_rc(export_errors ::: document_errors)
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   501
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   502
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   503
      build_errors match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   504
        case Exn.Res(build_errs) =>
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   505
          val errs = build_errs ::: document_errors
74259
6d48d6ba58df more robust: progress.stopped means that build has failed;
wenzelm
parents: 74258
diff changeset
   506
          if (errs.nonEmpty) {
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   507
            result.error_rc.output(
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   508
              errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   509
                errs.map(Protocol.Error_Message_Marker.apply))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   510
          }
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74259
diff changeset
   511
          else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt)
74259
6d48d6ba58df more robust: progress.stopped means that build has failed;
wenzelm
parents: 74258
diff changeset
   512
          else result
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   513
        case Exn.Exn(Exn.Interrupt()) =>
74306
a117c076aa22 clarified signature;
wenzelm
parents: 74259
diff changeset
   514
          if (result.ok) result.copy(rc = Process_Result.RC.interrupt)
74259
6d48d6ba58df more robust: progress.stopped means that build has failed;
wenzelm
parents: 74258
diff changeset
   515
          else result
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   516
        case Exn.Exn(exn) => throw exn
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   517
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   518
    }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   519
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   520
  def terminate(): Unit = future_result.cancel()
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   521
  def is_finished: Boolean = future_result.is_finished
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   522
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   523
  private val timeout_request: Option[Event_Timer.Request] =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   524
  {
73700
908351c8c0b1 check timeout_ignored as in ML, before applying timeout_scale;
wenzelm
parents: 73559
diff changeset
   525
    if (info.timeout_ignored) None
908351c8c0b1 check timeout_ignored as in ML, before applying timeout_scale;
wenzelm
parents: 73559
diff changeset
   526
    else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   527
  }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   528
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   529
  def join: (Process_Result, Option[String]) =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   530
  {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   531
    val result1 = future_result.join
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   532
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   533
    val was_timeout =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   534
      timeout_request match {
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   535
        case None => false
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   536
        case Some(request) => !request.cancel()
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   537
      }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   538
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   539
    val result2 =
73134
8a8ffe78eee7 clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents: 73033
diff changeset
   540
      if (result1.ok) result1
8a8ffe78eee7 clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents: 73033
diff changeset
   541
      else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc
8a8ffe78eee7 clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents: 73033
diff changeset
   542
      else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
72662
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   543
      else result1
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   544
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   545
    val heap_digest =
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   546
      if (result2.ok && do_store && store.output_heap(session_name).is_file)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   547
        Some(Sessions.write_heap_digest(store.output_heap(session_name)))
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   548
      else None
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   549
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   550
    (result2, heap_digest)
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   551
  }
5c08ad7adf77 clarified modules;
wenzelm
parents:
diff changeset
   552
}