src/Pure/Thy/sessions.scala
author wenzelm
Fri, 26 Aug 2022 21:28:26 +0200
changeset 75986 27d98da31985
parent 75984 75b65c1f7a1f
child 75987 ff2e67d73592
permissions -rw-r--r--
support 'chapter_definition' with description for presentation purposes;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/sessions.scala
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     3
65430
4433d189a77d tuned comment;
wenzelm
parents: 65429
diff changeset
     4
Cumulative session information.
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     5
*/
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     6
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
     8
65461
b6c2e30dc018 support for known theories files (according to multiple uses);
wenzelm
parents: 65457
diff changeset
     9
import java.io.{File => JFile}
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
    10
import java.nio.ByteBuffer
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
    11
import java.nio.channels.FileChannel
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
    12
import java.nio.file.StandardOpenOption
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
    13
import java.sql.SQLException
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
    14
73364
6bf6160a2c54 proper scala.collection.immutable;
wenzelm
parents: 73359
diff changeset
    15
import scala.collection.immutable.{SortedSet, SortedMap}
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
    16
import scala.collection.mutable
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
    17
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    19
object Sessions {
67284
0094d938c53b tuned signature;
wenzelm
parents: 67219
diff changeset
    20
  /* session and theory names */
62883
b04e9fe29223 clarified ML bootstrap;
wenzelm
parents: 62864
diff changeset
    21
72837
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    22
  val ROOTS: Path = Path.explode("ROOTS")
72832
03803bbfdca3 tuned signature;
wenzelm
parents: 72816
diff changeset
    23
  val ROOT: Path = Path.explode("ROOT")
03803bbfdca3 tuned signature;
wenzelm
parents: 72816
diff changeset
    24
72837
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    25
  val roots_name: String = "ROOTS"
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 67210
diff changeset
    26
  val root_name: String = "ROOT"
75406
85e8b4c2b9a9 clarified signature: avoid ambiguity in scala3;
wenzelm
parents: 75405
diff changeset
    27
  val theory_import: String = "Pure.Sessions"
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 67210
diff changeset
    28
69762
58fb0d779583 support for session information via virtual file-system;
wenzelm
parents: 69671
diff changeset
    29
  val UNSORTED = "Unsorted"
65445
e9e7f5f5794c more qualifier treatment, but in the end it is still ignored;
wenzelm
parents: 65441
diff changeset
    30
  val DRAFT = "Draft"
e9e7f5f5794c more qualifier treatment, but in the end it is still ignored;
wenzelm
parents: 65441
diff changeset
    31
65360
wenzelm
parents: 65359
diff changeset
    32
  def is_pure(name: String): Boolean = name == Thy_Header.PURE
64856
5e9bf964510a clarified modules;
wenzelm
parents: 63996
diff changeset
    33
75922
b327e5d5d6b4 tuned signature;
wenzelm
parents: 75921
diff changeset
    34
  def illegal_session(name: String): Boolean = name == "" || name == DRAFT
b327e5d5d6b4 tuned signature;
wenzelm
parents: 75921
diff changeset
    35
  def illegal_theory(name: String): Boolean = name == root_name || name == "bib"
67284
0094d938c53b tuned signature;
wenzelm
parents: 67219
diff changeset
    36
0094d938c53b tuned signature;
wenzelm
parents: 67219
diff changeset
    37
72837
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    38
  /* ROOTS file format */
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    39
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    40
  class File_Format extends isabelle.File_Format {
72837
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    41
    val format_name: String = roots_name
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    42
    val file_ext = ""
72839
a597300290de clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents: 72837
diff changeset
    43
a597300290de clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents: 72837
diff changeset
    44
    override def detect(name: String): Boolean =
a597300290de clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents: 72837
diff changeset
    45
      Thy_Header.split_file_name(name) match {
a597300290de clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents: 72837
diff changeset
    46
        case Some((_, file_name)) => file_name == roots_name
a597300290de clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents: 72837
diff changeset
    47
        case None => false
a597300290de clarified File_Format.detect: needs to operate on full node name;
wenzelm
parents: 72837
diff changeset
    48
      }
72837
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    49
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    50
    override def theory_suffix: String = "ROOTS_file"
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    51
    override def theory_content(name: String): String =
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    52
      """theory "ROOTS" imports Pure begin ROOTS_file """ +
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    53
        Outer_Syntax.quote_string(name) + """ end"""
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    54
  }
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    55
2c26c283f3ee PIDE support for session ROOTS;
wenzelm
parents: 72832
diff changeset
    56
67284
0094d938c53b tuned signature;
wenzelm
parents: 67219
diff changeset
    57
  /* base info and source dependencies */
0094d938c53b tuned signature;
wenzelm
parents: 67219
diff changeset
    58
65495
60d4fbed2b1f tuned signature;
wenzelm
parents: 65490
diff changeset
    59
  sealed case class Base(
75750
2eee2fdfb6e2 clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
wenzelm
parents: 75749
diff changeset
    60
    session_name: String = "",
75749
45fc58d48e4a tuned signature;
wenzelm
parents: 75748
diff changeset
    61
    session_pos: Position.T = Position.none,
75748
b6d74c90b588 clarified signature;
wenzelm
parents: 75744
diff changeset
    62
    proper_session_theories: List[Document.Node.Name] = Nil,
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
    63
    document_theories: List[Document.Node.Name] = Nil,
75740
d22ae56ca00c tuned comments;
wenzelm
parents: 75739
diff changeset
    64
    loaded_theories: Graph[String, Outer_Syntax] = Graph.string,  // cumulative imports
d22ae56ca00c tuned comments;
wenzelm
parents: 75739
diff changeset
    65
    used_theories: List[(Document.Node.Name, Options)] = Nil,  // new imports
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
    66
    load_commands: Map[Document.Node.Name, List[Command_Span.Span]] = Map.empty,
70740
525c18b8ed53 clarified data structures;
wenzelm
parents: 70739
diff changeset
    67
    known_theories: Map[String, Document.Node.Entry] = Map.empty,
525c18b8ed53 clarified data structures;
wenzelm
parents: 70739
diff changeset
    68
    known_loaded_files: Map[String, List[Path]] = Map.empty,
66720
b07192253605 tuned signature;
wenzelm
parents: 66719
diff changeset
    69
    overall_syntax: Outer_Syntax = Outer_Syntax.empty,
66744
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
    70
    imported_sources: List[(Path, SHA1.Digest)] = Nil,
75741
17b1c4fbc008 tuned signature;
wenzelm
parents: 75740
diff changeset
    71
    session_sources: List[(Path, SHA1.Digest)] = Nil,
66822
4642cf4a7ebb tuned signature;
wenzelm
parents: 66819
diff changeset
    72
    session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    73
    errors: List[String] = Nil
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    74
  ) {
75885
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
    75
    def session_entry: (String, Base) = session_name -> this
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
    76
69102
4b06a20b13b5 tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;
wenzelm
parents: 69080
diff changeset
    77
    override def toString: String =
75750
2eee2fdfb6e2 clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
wenzelm
parents: 75749
diff changeset
    78
      "Sessions.Base(session_name = " + quote(session_name) +
2eee2fdfb6e2 clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
wenzelm
parents: 75749
diff changeset
    79
        ", loaded_theories = " + loaded_theories.size +
69102
4b06a20b13b5 tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;
wenzelm
parents: 69080
diff changeset
    80
        ", used_theories = " + used_theories.length + ")"
4b06a20b13b5 tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;
wenzelm
parents: 69080
diff changeset
    81
66717
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66716
diff changeset
    82
    def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 66701
diff changeset
    83
    def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
65432
wenzelm
parents: 65430
diff changeset
    84
66717
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66716
diff changeset
    85
    def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66716
diff changeset
    86
      if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66716
diff changeset
    87
    def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66716
diff changeset
    88
      loaded_theory_syntax(name.theory)
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66716
diff changeset
    89
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72666
diff changeset
    90
    def theory_syntax(name: Document.Node.Name): Outer_Syntax =
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72666
diff changeset
    91
      loaded_theory_syntax(name) getOrElse overall_syntax
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72666
diff changeset
    92
66770
122df1fde073 clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
wenzelm
parents: 66764
diff changeset
    93
    def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
122df1fde073 clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
wenzelm
parents: 66764
diff changeset
    94
      nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
65355
403eabd73c9a tuned signature;
wenzelm
parents: 65326
diff changeset
    95
  }
64856
5e9bf964510a clarified modules;
wenzelm
parents: 63996
diff changeset
    96
75885
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
    97
  val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
    98
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    99
  sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
69102
4b06a20b13b5 tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;
wenzelm
parents: 69080
diff changeset
   100
    override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
4b06a20b13b5 tuned output -- avoid bombing of Scala toplevel, e.g. for AFP deps;
wenzelm
parents: 69080
diff changeset
   101
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   102
    def is_empty: Boolean = session_bases.isEmpty
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   103
    def apply(name: String): Base = session_bases(name)
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   104
    def get(name: String): Option[Base] = session_bases.get(name)
66744
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
   105
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
   106
    def imported_sources(name: String): List[SHA1.Digest] =
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
   107
      session_bases(name).imported_sources.map(_._2)
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
   108
75741
17b1c4fbc008 tuned signature;
wenzelm
parents: 75740
diff changeset
   109
    def session_sources(name: String): List[SHA1.Digest] =
17b1c4fbc008 tuned signature;
wenzelm
parents: 75740
diff changeset
   110
      session_bases(name).session_sources.map(_._2)
66571
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   111
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   112
    def errors: List[String] =
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   113
      (for {
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   114
        (name, base) <- session_bases.iterator
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   115
        if base.errors.nonEmpty
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   116
      } yield cat_lines(base.errors) +
75749
45fc58d48e4a tuned signature;
wenzelm
parents: 75748
diff changeset
   117
          "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.session_pos)
66571
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   118
      ).toList
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   119
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   120
    def check_errors: Deps =
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   121
      errors match {
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   122
        case Nil => this
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   123
        case errs => error(cat_lines(errs))
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   124
      }
75774
efc25bf4b795 discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents: 75773
diff changeset
   125
efc25bf4b795 discontinued Export.Provider in favour of Export.Context and its derivatives;
wenzelm
parents: 75773
diff changeset
   126
    def base_info(session: String): Base_Info =
75777
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   127
      Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors)
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   128
  }
64856
5e9bf964510a clarified modules;
wenzelm
parents: 63996
diff changeset
   129
67052
caf87d4b9b61 tuned signature;
wenzelm
parents: 67029
diff changeset
   130
  def deps(sessions_structure: Structure,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   131
    progress: Progress = new Progress,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   132
    inlined_files: Boolean = false,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   133
    verbose: Boolean = false,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   134
    list_files: Boolean = false,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   135
    check_keywords: Set[String] = Set.empty
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   136
  ): Deps = {
66743
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   137
    var cache_sources = Map.empty[JFile, SHA1.Digest]
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   138
    def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
66743
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   139
      for {
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   140
        path <- paths
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   141
        file = path.file
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   142
        if cache_sources.isDefinedAt(file) || file.isFile
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   143
      }
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   144
      yield {
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   145
        cache_sources.get(file) match {
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   146
          case Some(digest) => (path, digest)
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   147
          case None =>
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   148
            val digest = SHA1.digest(file)
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   149
            cache_sources = cache_sources + (file -> digest)
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   150
            (path, digest)
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   151
        }
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   152
      }
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   153
    }
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   154
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   155
    val session_bases =
75885
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
   156
      sessions_structure.imports_topological_order.foldLeft(
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
   157
          Map(Sessions.bootstrap_base.session_entry)) {
67023
e27e05d6f2a7 tuned signature;
wenzelm
parents: 67018
diff changeset
   158
        case (session_bases, session_name) =>
67880
e59220a075de tuned signature;
wenzelm
parents: 67869
diff changeset
   159
          progress.expose_interrupt()
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   160
67024
wenzelm
parents: 67023
diff changeset
   161
          val info = sessions_structure(session_name)
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   162
          try {
72066
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   163
            val deps_base = info.deps_base(session_bases)
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   164
            val resources = new Resources(sessions_structure, deps_base)
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   165
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   166
            if (verbose || list_files) {
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   167
              val groups =
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   168
                if (info.groups.isEmpty) ""
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   169
                else info.groups.mkString(" (", " ", ")")
75977
59aa034220bf more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
wenzelm
parents: 75967
diff changeset
   170
              progress.echo("Session " + info.chapter + "/" + session_name + groups)
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   171
            }
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   172
69008
d55783ea6cf6 more detailed session dependencies, with conditions for theories;
wenzelm
parents: 68841
diff changeset
   173
            val dependencies = resources.session_dependencies(info)
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   174
67053
wenzelm
parents: 67052
diff changeset
   175
            val overall_syntax = dependencies.overall_syntax
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   176
75748
b6d74c90b588 clarified signature;
wenzelm
parents: 75744
diff changeset
   177
            val proper_session_theories =
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   178
              dependencies.theories.filter(name =>
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   179
                sessions_structure.theory_qualifier(name) == session_name)
72323
e36f94e2eb6b some support for document preparation in Isabelle/Scala;
wenzelm
parents: 72068
diff changeset
   180
67059
df7d728103f1 tuned signature;
wenzelm
parents: 67053
diff changeset
   181
            val theory_files = dependencies.theories.map(_.path)
72068
4768b1facec2 clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);
wenzelm
parents: 72067
diff changeset
   182
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   183
            val (load_commands, load_commands_errors) =
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   184
              try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) }
72068
4768b1facec2 clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);
wenzelm
parents: 72067
diff changeset
   185
              catch { case ERROR(msg) => (Nil, List(msg)) }
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   186
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   187
            val loaded_files =
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   188
              load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) })
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   189
66742
wenzelm
parents: 66737
diff changeset
   190
            val session_files =
66701
d181f8a0e857 maintain loaded_files for each theory;
wenzelm
parents: 66696
diff changeset
   191
              (theory_files ::: loaded_files.flatMap(_._2) :::
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   192
                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   193
67053
wenzelm
parents: 67052
diff changeset
   194
            val imported_files = if (inlined_files) dependencies.imported_files else Nil
66743
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   195
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   196
            if (list_files)
66742
wenzelm
parents: 66737
diff changeset
   197
              progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   198
66719
d37efafd55b5 clarified theory syntax vs. overall session syntax;
wenzelm
parents: 66718
diff changeset
   199
            if (check_keywords.nonEmpty) {
d37efafd55b5 clarified theory syntax vs. overall session syntax;
wenzelm
parents: 66718
diff changeset
   200
              Check_Keywords.check_keywords(
66720
b07192253605 tuned signature;
wenzelm
parents: 66719
diff changeset
   201
                progress, overall_syntax.keywords, check_keywords, theory_files)
66719
d37efafd55b5 clarified theory syntax vs. overall session syntax;
wenzelm
parents: 66718
diff changeset
   202
            }
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   203
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   204
            val session_graph_display: Graph_Display.Graph = {
65507
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   205
              def session_node(name: String): Graph_Display.Node =
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   206
                Graph_Display.Node("[" + name + "]", "session." + name)
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   207
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   208
              def node(name: Document.Node.Name): Graph_Display.Node = {
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   209
                val qualifier = sessions_structure.theory_qualifier(name)
66780
bf54ca580bf2 theory qualifier is always session name (see also 31e8a86971a8);
wenzelm
parents: 66770
diff changeset
   210
                if (qualifier == info.name)
65507
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   211
                  Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
65528
d15d302da7f0 proper theory_qualifier;
wenzelm
parents: 65525
diff changeset
   212
                else session_node(qualifier)
65507
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   213
              }
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   214
70946
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   215
              val required_sessions =
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   216
                dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   217
                  .map(theory => sessions_structure.theory_qualifier(theory))
71574
95460356d633 avoid premature crash due to missing session parents/imports;
wenzelm
parents: 71569
diff changeset
   218
                  .filter(name => name != info.name && sessions_structure.defined(name))
70946
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   219
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   220
              val required_subgraph =
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   221
                sessions_structure.imports_graph
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   222
                  .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet)
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   223
                  .transitive_closure
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   224
                  .restrict(required_sessions.toSet)
79d23e6436d0 clarified session_graph_display: restrict sessions to actually required theories;
wenzelm
parents: 70869
diff changeset
   225
                  .transitive_reduction_acyclic
65507
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   226
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   227
              val graph0 =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   228
                required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   229
                  case (g, session) =>
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   230
                    val a = session_node(session)
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   231
                    val bs = required_subgraph.imm_preds(session).toList.map(session_node)
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   232
                    bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   233
                }
65507
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   234
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   235
              dependencies.entries.foldLeft(graph0) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   236
                case (g, entry) =>
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   237
                  val a = node(entry.name)
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   238
                  val bs = entry.header.imports.map(node).filterNot(_ == a)
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   239
                  bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   240
              }
65507
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   241
            }
decdb95bd007 clarified session graph: collapse theories from other sessions;
wenzelm
parents: 65500
diff changeset
   242
70740
525c18b8ed53 clarified data structures;
wenzelm
parents: 70739
diff changeset
   243
            val known_theories =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   244
              dependencies.entries.iterator.map(entry => entry.name.theory -> entry).
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   245
                foldLeft(deps_base.known_theories)(_ + _)
70740
525c18b8ed53 clarified data structures;
wenzelm
parents: 70739
diff changeset
   246
72066
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   247
            val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
66701
d181f8a0e857 maintain loaded_files for each theory;
wenzelm
parents: 66696
diff changeset
   248
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   249
            val import_errors = {
72067
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   250
              val known_sessions =
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   251
                sessions_structure.imports_requirements(List(session_name)).toSet
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   252
              for {
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   253
                name <- dependencies.theories
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   254
                qualifier = sessions_structure.theory_qualifier(name)
72067
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   255
                if !known_sessions(qualifier)
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   256
              } yield "Bad import of theory " + quote(name.toString) +
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   257
                ": need to include sessions " + quote(qualifier) + " in ROOT"
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   258
            }
17507b48b6f5 clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
wenzelm
parents: 72066
diff changeset
   259
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   260
            val document_errors =
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   261
              info.document_theories.flatMap(
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   262
              {
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   263
                case (thy, pos) =>
74812
wenzelm
parents: 74810
diff changeset
   264
                  val build_hierarchy =
72647
fd6dc1a4b9ca more robust, e.g. for "isabelle build_doc system";
wenzelm
parents: 72634
diff changeset
   265
                    if (sessions_structure.build_graph.defined(session_name)) {
74812
wenzelm
parents: 74810
diff changeset
   266
                      sessions_structure.build_hierarchy(session_name)
72647
fd6dc1a4b9ca more robust, e.g. for "isabelle build_doc system";
wenzelm
parents: 72634
diff changeset
   267
                    }
fd6dc1a4b9ca more robust, e.g. for "isabelle build_doc system";
wenzelm
parents: 72634
diff changeset
   268
                    else Nil
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   269
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   270
                  def err(msg: String): Option[String] =
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   271
                    Some(msg + " " + quote(thy) + Position.here(pos))
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   272
72604
wenzelm
parents: 72603
diff changeset
   273
                  known_theories.get(thy).map(_.name) match {
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   274
                    case None => err("Unknown document theory")
72604
wenzelm
parents: 72603
diff changeset
   275
                    case Some(name) =>
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   276
                      val qualifier = sessions_structure.theory_qualifier(name)
75748
b6d74c90b588 clarified signature;
wenzelm
parents: 75744
diff changeset
   277
                      if (proper_session_theories.contains(name)) {
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   278
                        err("Redundant document theory from this session:")
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   279
                      }
74812
wenzelm
parents: 74810
diff changeset
   280
                      else if (build_hierarchy.contains(qualifier)) None
72604
wenzelm
parents: 72603
diff changeset
   281
                      else if (dependencies.theories.contains(name)) None
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   282
                      else err("Document theory from other session not imported properly:")
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   283
                  }
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   284
              })
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   285
            val document_theories =
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   286
              info.document_theories.map({ case (thy, _) => known_theories(thy).name })
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   287
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   288
            val dir_errors = {
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   289
              val ok = info.dirs.map(_.canonical_file).toSet
70679
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   290
              val bad =
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   291
                (for {
75748
b6d74c90b588 clarified signature;
wenzelm
parents: 75744
diff changeset
   292
                  name <- proper_session_theories.iterator
70719
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   293
                  path = name.master_dir_path
70676
73812c598a26 check session directories;
wenzelm
parents: 70674
diff changeset
   294
                  if !ok(path.canonical_file)
70679
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   295
                  path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   296
                } yield (path1, name)).toList
71602
wenzelm
parents: 71601
diff changeset
   297
              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
70679
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   298
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   299
              val errs1 =
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   300
                for { (path1, name) <- bad }
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   301
                yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   302
              val errs2 =
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   303
                if (bad_dirs.isEmpty) Nil
7b6e6d61204a clarified messages;
wenzelm
parents: 70678
diff changeset
   304
                else List("Implicit use of session directories: " + commas(bad_dirs))
70693
0fec12eabad0 session directories need to exist;
wenzelm
parents: 70687
diff changeset
   305
              val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
70719
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   306
              val errs4 =
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   307
                (for {
75748
b6d74c90b588 clarified signature;
wenzelm
parents: 75744
diff changeset
   308
                  name <- proper_session_theories.iterator
70719
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   309
                  name1 <- resources.find_theory_node(name.theory)
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   310
                  if name.node != name1.node
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   311
                } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   312
                .toList
70693
0fec12eabad0 session directories need to exist;
wenzelm
parents: 70687
diff changeset
   313
70719
b3f61e166763 more errors;
wenzelm
parents: 70715
diff changeset
   314
              errs1 ::: errs2 ::: errs3 ::: errs4
70676
73812c598a26 check session directories;
wenzelm
parents: 70674
diff changeset
   315
            }
73812c598a26 check session directories;
wenzelm
parents: 70674
diff changeset
   316
66743
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   317
            val sources_errors =
ff05d922bc34 cache sources: invoke SHA1.digest at most once;
wenzelm
parents: 66742
diff changeset
   318
              for (p <- session_files if !p.is_file) yield "No such file: " + p
66604
1af360d1cad2 tolerate more errors (cf. 1e5ae735e026);
wenzelm
parents: 66575
diff changeset
   319
69904
6f5bd59f75f4 more sanity checks;
wenzelm
parents: 69857
diff changeset
   320
            val path_errors =
6f5bd59f75f4 more sanity checks;
wenzelm
parents: 69857
diff changeset
   321
              try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
6f5bd59f75f4 more sanity checks;
wenzelm
parents: 69857
diff changeset
   322
              catch { case ERROR(msg) => List(msg) }
6f5bd59f75f4 more sanity checks;
wenzelm
parents: 69857
diff changeset
   323
67297
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   324
            val bibtex_errors =
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   325
              try { info.bibtex_entries; Nil }
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   326
              catch { case ERROR(msg) => List(msg) }
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   327
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   328
            val base =
66571
0fdeb24e535e clarified errors;
wenzelm
parents: 66243
diff changeset
   329
              Base(
75750
2eee2fdfb6e2 clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
wenzelm
parents: 75749
diff changeset
   330
                session_name = info.name,
75749
45fc58d48e4a tuned signature;
wenzelm
parents: 75748
diff changeset
   331
                session_pos = info.pos,
75748
b6d74c90b588 clarified signature;
wenzelm
parents: 75744
diff changeset
   332
                proper_session_theories = proper_session_theories,
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   333
                document_theories = document_theories,
67053
wenzelm
parents: 67052
diff changeset
   334
                loaded_theories = dependencies.loaded_theories,
72062
d0909b5d88eb tuned signature;
wenzelm
parents: 71971
diff changeset
   335
                used_theories = dependencies.theories_adjunct,
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   336
                load_commands = load_commands.toMap,
70740
525c18b8ed53 clarified data structures;
wenzelm
parents: 70739
diff changeset
   337
                known_theories = known_theories,
525c18b8ed53 clarified data structures;
wenzelm
parents: 70739
diff changeset
   338
                known_loaded_files = known_loaded_files,
66720
b07192253605 tuned signature;
wenzelm
parents: 66719
diff changeset
   339
                overall_syntax = overall_syntax,
66744
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
   340
                imported_sources = check_sources(imported_files),
75741
17b1c4fbc008 tuned signature;
wenzelm
parents: 75740
diff changeset
   341
                session_sources = check_sources(session_files),
66822
4642cf4a7ebb tuned signature;
wenzelm
parents: 66819
diff changeset
   342
                session_graph_display = session_graph_display,
72816
ea4f86914cb2 support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents: 72799
diff changeset
   343
                errors = dependencies.errors ::: load_commands_errors ::: import_errors :::
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   344
                  document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   345
                  bibtex_errors)
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   346
75885
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
   347
            session_bases + base.session_entry
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   348
          }
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   349
          catch {
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   350
            case ERROR(msg) =>
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   351
              cat_error(msg, "The error(s) above occurred in session " +
65519
d244d8f8e13f store Sessions.Info.name;
wenzelm
parents: 65517
diff changeset
   352
                quote(info.name) + Position.here(info.pos))
65463
104502de757c more informative known_files: known_theories within the local session directory come first;
wenzelm
parents: 65461
diff changeset
   353
          }
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   354
      }
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   355
70686
9cde8c4ea5a5 discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents: 70685
diff changeset
   356
    Deps(sessions_structure, session_bases)
65372
b722ee40c26c refer to global_theories from all sessions, before selection;
wenzelm
parents: 65371
diff changeset
   357
  }
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   358
66963
1c3d0c12bb51 clarified signature;
wenzelm
parents: 66962
diff changeset
   359
1c3d0c12bb51 clarified signature;
wenzelm
parents: 66962
diff changeset
   360
  /* base info */
1c3d0c12bb51 clarified signature;
wenzelm
parents: 66962
diff changeset
   361
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   362
  sealed case class Base_Info(
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   363
    base: Base,
75777
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   364
    sessions_structure: Structure = Structure.empty,
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   365
    errors: List[String] = Nil,
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   366
    infos: List[Info] = Nil
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   367
  ) {
75921
423021c98500 clarified signature: Sessions.Base_Info follows Sessions.Base;
wenzelm
parents: 75920
diff changeset
   368
    def session_name: String = base.session_name
75920
27bf2533f4a4 clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
wenzelm
parents: 75917
diff changeset
   369
27bf2533f4a4 clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
wenzelm
parents: 75917
diff changeset
   370
    def check_errors: Base_Info =
27bf2533f4a4 clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
wenzelm
parents: 75917
diff changeset
   371
      if (errors.isEmpty) this
27bf2533f4a4 clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
wenzelm
parents: 75917
diff changeset
   372
      else error(cat_lines(errors))
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   373
  }
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   374
75779
5470c67bd772 clarified signature: prefer Export.Session_Context;
wenzelm
parents: 75777
diff changeset
   375
  def base_info0(session: String): Base_Info =
75777
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   376
    Base_Info(Base(session_name = session))
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   377
67846
wenzelm
parents: 67493
diff changeset
   378
  def base_info(options: Options,
wenzelm
parents: 67493
diff changeset
   379
    session: String,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71642
diff changeset
   380
    progress: Progress = new Progress,
65428
f8dd71a0791a support for all_known_theories of all sessions;
wenzelm
parents: 65427
diff changeset
   381
    dirs: List[Path] = Nil,
67922
9e668ae81f97 clarified signature: prefer selective include_sessions;
wenzelm
parents: 67880
diff changeset
   382
    include_sessions: List[String] = Nil,
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 68318
diff changeset
   383
    session_ancestor: Option[String] = None,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   384
    session_requirements: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   385
  ): Base_Info = {
67026
687c822ee5e3 tuned signature;
wenzelm
parents: 67025
diff changeset
   386
    val full_sessions = load_structure(options, dirs = dirs)
65372
b722ee40c26c refer to global_theories from all sessions, before selection;
wenzelm
parents: 65371
diff changeset
   387
66990
b23adab22e67 allow unrelated ancestor;
wenzelm
parents: 66988
diff changeset
   388
    val selected_sessions =
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 68318
diff changeset
   389
      full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   390
    val info = selected_sessions(session)
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 68318
diff changeset
   391
    val ancestor = session_ancestor orElse info.parent
66963
1c3d0c12bb51 clarified signature;
wenzelm
parents: 66962
diff changeset
   392
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   393
    val (session1, infos1) =
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 68318
diff changeset
   394
      if (session_requirements && ancestor.isDefined) {
70671
cb1776c8e216 clarified signature: retain global session information, unaffected by later restriction;
wenzelm
parents: 70668
diff changeset
   395
        val deps = Sessions.deps(selected_sessions, progress = progress)
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   396
        val base = deps(session)
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   397
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   398
        val ancestor_loaded =
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   399
          deps.get(ancestor.get) match {
66990
b23adab22e67 allow unrelated ancestor;
wenzelm
parents: 66988
diff changeset
   400
            case Some(ancestor_base)
b23adab22e67 allow unrelated ancestor;
wenzelm
parents: 66988
diff changeset
   401
            if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71599
diff changeset
   402
              ancestor_base.loaded_theories.defined _
66990
b23adab22e67 allow unrelated ancestor;
wenzelm
parents: 66988
diff changeset
   403
            case _ =>
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   404
              error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   405
          }
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   406
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   407
        val required_theories =
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   408
          for {
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   409
            thy <- base.loaded_theories.keys
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   410
            if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   411
          }
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   412
          yield thy
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   413
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   414
        if (required_theories.isEmpty) (ancestor.get, Nil)
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   415
        else {
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 68318
diff changeset
   416
          val other_name = info.name + "_requirements(" + ancestor.get + ")"
71569
391ea80ff27c more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);
wenzelm
parents: 70946
diff changeset
   417
          Isabelle_System.isabelle_tmp_prefix()
391ea80ff27c more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);
wenzelm
parents: 70946
diff changeset
   418
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   419
          (other_name,
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   420
            List(
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   421
              make_info(info.options,
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   422
                dir_selected = false,
70685
c1597167563e avoid duplicate directories wrt. synthetic session;
wenzelm
parents: 70684
diff changeset
   423
                dir = Path.explode("$ISABELLE_TMP_PREFIX"),
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   424
                chapter = info.chapter,
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   425
                Session_Entry(
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   426
                  pos = info.pos,
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   427
                  name = other_name,
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   428
                  groups = info.groups,
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   429
                  path = ".",
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   430
                  parent = ancestor,
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   431
                  description = "Required theory imports from other sessions",
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   432
                  options = Nil,
66991
fc87d3becd69 proper deps;
wenzelm
parents: 66990
diff changeset
   433
                  imports = info.deps,
70678
36c8c32346cb clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents: 70676
diff changeset
   434
                  directories = Nil,
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   435
                  theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   436
                  document_theories = Nil,
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   437
                  document_files = Nil,
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   438
                  export_files = Nil,
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   439
                  export_classpath = Nil))))
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   440
        }
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   441
      }
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   442
      else (session, Nil)
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
   443
66974
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   444
    val full_sessions1 =
b14c24b31f45 avoid duplicate invocation of expensive Sessions.deps on full_sessions;
wenzelm
parents: 66970
diff changeset
   445
      if (infos1.isEmpty) full_sessions
67026
687c822ee5e3 tuned signature;
wenzelm
parents: 67025
diff changeset
   446
      else load_structure(options, dirs = dirs, infos = infos1)
66987
352b23c97ac8 support focus_session, for much faster startup of Isabelle/jEdit;
wenzelm
parents: 66984
diff changeset
   447
352b23c97ac8 support focus_session, for much faster startup of Isabelle/jEdit;
wenzelm
parents: 66984
diff changeset
   448
    val selected_sessions1 =
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   449
      full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
66964
9f2de457b95e clarified signature;
wenzelm
parents: 66963
diff changeset
   450
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   451
    val deps1 = Sessions.deps(selected_sessions1, progress = progress)
66964
9f2de457b95e clarified signature;
wenzelm
parents: 66963
diff changeset
   452
75777
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   453
    Base_Info(deps1(session1), sessions_structure = full_sessions1,
ed32b5554ed3 clarified signature;
wenzelm
parents: 75775
diff changeset
   454
      errors = deps1.errors, infos = infos1)
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   455
  }
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   456
4b0a43afc3fb clarified modules;
wenzelm
parents: 64856
diff changeset
   457
65415
8cd54b18b68b clarified signature: tree structure is not essential;
wenzelm
parents: 65410
diff changeset
   458
  /* cumulative session info */
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   459
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   460
  sealed case class Info(
65519
d244d8f8e13f store Sessions.Info.name;
wenzelm
parents: 65517
diff changeset
   461
    name: String,
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   462
    chapter: String,
66829
5baca4c94737 tuned signature;
wenzelm
parents: 66828
diff changeset
   463
    dir_selected: Boolean,
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   464
    pos: Position.T,
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   465
    groups: List[String],
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   466
    dir: Path,
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   467
    parent: Option[String],
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   468
    description: String,
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   469
    directories: List[Path],
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   470
    options: Options,
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   471
    imports: List[String],
65517
1544e61e5314 more position information;
wenzelm
parents: 65507
diff changeset
   472
    theories: List[(Options, List[(String, Position.T)])],
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65373
diff changeset
   473
    global_theories: List[String],
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   474
    document_theories: List[(String, Position.T)],
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   475
    document_files: List[(Path, Path)],
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69560
diff changeset
   476
    export_files: List[(Path, Int, List[String])],
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   477
    export_classpath: List[String],
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   478
    meta_digest: SHA1.Digest
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   479
  ) {
66828
3c936ebebc23 tuned signature;
wenzelm
parents: 66823
diff changeset
   480
    def deps: List[String] = parent.toList ::: imports
3c936ebebc23 tuned signature;
wenzelm
parents: 66823
diff changeset
   481
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   482
    def deps_base(session_bases: String => Base): Base = {
72066
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   483
      val parent_base = session_bases(parent.getOrElse(""))
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   484
      val imports_bases = imports.map(session_bases)
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   485
      parent_base.copy(
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   486
        known_theories =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   487
          (for {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   488
            base <- imports_bases.iterator
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   489
            (_, entry) <- base.known_theories.iterator
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   490
          } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _),
72066
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   491
        known_loaded_files =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   492
          imports_bases.iterator.map(_.known_loaded_files).
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   493
            foldLeft(parent_base.known_loaded_files)(_ ++ _))
72066
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   494
    }
ba5b37671528 clarified signature;
wenzelm
parents: 72065
diff changeset
   495
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   496
    def dirs: List[Path] = dir :: directories
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   497
73701
d83e7e444b43 ignore session build timeout, notably in AFP;
wenzelm
parents: 73700
diff changeset
   498
    def timeout_ignored: Boolean =
d83e7e444b43 ignore session build timeout, notably in AFP;
wenzelm
parents: 73700
diff changeset
   499
      !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
d83e7e444b43 ignore session build timeout, notably in AFP;
wenzelm
parents: 73700
diff changeset
   500
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   501
    def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
67297
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   502
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   503
    def document_enabled: Boolean =
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   504
      options.string("document") match {
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   505
        case "" | "false" => false
73826
72900f34dbb3 allow system option short form NAME for NAME=true for type string, not just bool;
wenzelm
parents: 73815
diff changeset
   506
        case "pdf" | "true" => true
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   507
        case doc => error("Bad document specification " + quote(doc))
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   508
      }
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   509
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   510
    def document_variants: List[Document_Build.Document_Variant] = {
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   511
      val variants =
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   512
        Library.space_explode(':', options.string("document_variants")).
73718
ecb31c3bf980 clarified modules;
wenzelm
parents: 73701
diff changeset
   513
          map(Document_Build.Document_Variant.parse)
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   514
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   515
      val dups = Library.duplicates(variants.map(_.name))
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   516
      if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   517
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   518
      variants
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   519
    }
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   520
75902
0f46e06030e9 tuned signature;
wenzelm
parents: 75890
diff changeset
   521
    def document_echo: Boolean = options.bool("document_echo")
0f46e06030e9 tuned signature;
wenzelm
parents: 75890
diff changeset
   522
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   523
    def documents: List[Document_Build.Document_Variant] = {
72672
573ccec4dbac tuned signature;
wenzelm
parents: 72670
diff changeset
   524
      val variants = document_variants
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   525
      if (!document_enabled || document_files.isEmpty) Nil else variants
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   526
    }
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   527
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   528
    def document_output: Option[Path] =
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   529
      options.string("document_output") match {
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   530
        case "" => None
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   531
        case s => Some(dir + Path.explode(s))
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   532
      }
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72571
diff changeset
   533
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72647
diff changeset
   534
    def browser_info: Boolean = options.bool("browser_info")
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72647
diff changeset
   535
72613
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   536
    lazy val bibtex_entries: List[Text.Info[String]] =
67297
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   537
      (for {
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   538
        (document_dir, file) <- document_files.iterator
75906
2167b9e3157a clarified signature: support for adhoc file types;
wenzelm
parents: 75902
diff changeset
   539
        if File.is_bib(file.file_name)
67297
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   540
        info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
86a099f896fc formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents: 67290
diff changeset
   541
      } yield info).toList
70859
6e6254bbce1f split into standard partitions, for improved scalability;
wenzelm
parents: 70796
diff changeset
   542
70869
1d063b7f7928 incorporate sessions with record_proofs;
wenzelm
parents: 70867
diff changeset
   543
    def record_proofs: Boolean = options.int("record_proofs") >= 2
1d063b7f7928 incorporate sessions with record_proofs;
wenzelm
parents: 70867
diff changeset
   544
70859
6e6254bbce1f split into standard partitions, for improved scalability;
wenzelm
parents: 70796
diff changeset
   545
    def is_afp: Boolean = chapter == AFP.chapter
6e6254bbce1f split into standard partitions, for improved scalability;
wenzelm
parents: 70796
diff changeset
   546
    def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   547
  }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   548
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   549
  def make_info(
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   550
    options: Options,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   551
    dir_selected: Boolean,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   552
    dir: Path,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   553
    chapter: String,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   554
    entry: Session_Entry
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   555
  ): Info = {
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   556
    try {
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   557
      val name = entry.name
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   558
75922
b327e5d5d6b4 tuned signature;
wenzelm
parents: 75921
diff changeset
   559
      if (illegal_session(name)) error("Illegal session name " + quote(name))
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   560
      if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   561
      if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   562
70672
e4bba654d085 clarified session_directories: relative to session_path, with overlapping information;
wenzelm
parents: 70671
diff changeset
   563
      val session_path = dir + Path.explode(entry.path)
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   564
      val directories = entry.directories.map(dir => session_path + Path.explode(dir))
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   565
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   566
      val session_options = options ++ entry.options
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   567
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   568
      val theories =
67216
99815211970c disallow theory name "ROOT";
wenzelm
parents: 67215
diff changeset
   569
        entry.theories.map({ case (opts, thys) =>
99815211970c disallow theory name "ROOT";
wenzelm
parents: 67215
diff changeset
   570
          (session_options ++ opts,
99815211970c disallow theory name "ROOT";
wenzelm
parents: 67215
diff changeset
   571
            thys.map({ case ((thy, pos), _) =>
75923
e4ada7b9e328 more thorough check, without path name artifacts (e.g. "./README");
wenzelm
parents: 75922
diff changeset
   572
              val thy_name = Thy_Header.import_name(thy)
e4ada7b9e328 more thorough check, without path name artifacts (e.g. "./README");
wenzelm
parents: 75922
diff changeset
   573
              if (illegal_theory(thy_name)) {
e4ada7b9e328 more thorough check, without path name artifacts (e.g. "./README");
wenzelm
parents: 75922
diff changeset
   574
                error("Illegal theory name " + quote(thy_name) + Position.here(pos))
75922
b327e5d5d6b4 tuned signature;
wenzelm
parents: 75921
diff changeset
   575
              }
67216
99815211970c disallow theory name "ROOT";
wenzelm
parents: 67215
diff changeset
   576
              else (thy, pos) })) })
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   577
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   578
      val global_theories =
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   579
        for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   580
        yield {
69366
b6dacf6eabe3 clarified signature;
wenzelm
parents: 69255
diff changeset
   581
          val thy_name = Path.explode(thy).file_name
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   582
          if (Long_Name.is_qualified(thy_name))
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   583
            error("Bad qualified name for global theory " +
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   584
              quote(thy_name) + Position.here(pos))
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   585
          else thy_name
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   586
        }
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   587
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   588
      val conditions =
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   589
        theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   590
          map(x => (x, Isabelle_System.getenv(x) != ""))
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   591
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   592
      val document_files =
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   593
        entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   594
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   595
      val export_files =
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69560
diff changeset
   596
        entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   597
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   598
      val meta_digest =
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   599
        SHA1.digest(
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   600
          (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
72666
945cee776e79 proper meta_digest: avoid non-portable position information;
wenzelm
parents: 72653
diff changeset
   601
            entry.theories_no_position, conditions, entry.document_theories_no_position,
945cee776e79 proper meta_digest: avoid non-portable position information;
wenzelm
parents: 72653
diff changeset
   602
            entry.document_files)
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   603
          .toString)
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   604
70672
e4bba654d085 clarified session_directories: relative to session_path, with overlapping information;
wenzelm
parents: 70671
diff changeset
   605
      Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   606
        entry.parent, entry.description, directories, session_options,
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   607
        entry.imports, theories, global_theories, entry.document_theories, document_files,
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   608
        export_files, entry.export_classpath, meta_digest)
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   609
    }
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   610
    catch {
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   611
      case ERROR(msg) =>
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   612
        error(msg + "\nThe error(s) above occurred in session entry " +
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   613
          quote(entry.name) + Position.here(entry.pos))
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   614
    }
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   615
  }
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
   616
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   617
  object Selection {
65422
b606c98e6d10 tuned signature;
wenzelm
parents: 65420
diff changeset
   618
    val empty: Selection = Selection()
65525
360063716c71 more operations;
wenzelm
parents: 65524
diff changeset
   619
    val all: Selection = Selection(all_sessions = true)
70788
b254a95b6e77 tuned signature;
wenzelm
parents: 70740
diff changeset
   620
    def session(session: String): Selection = Selection(sessions = List(session))
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   621
  }
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   622
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   623
  sealed case class Selection(
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   624
    requirements: Boolean = false,
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   625
    all_sessions: Boolean = false,
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66736
diff changeset
   626
    base_sessions: List[String] = Nil,
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   627
    exclude_session_groups: List[String] = Nil,
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   628
    exclude_sessions: List[String] = Nil,
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   629
    session_groups: List[String] = Nil,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   630
    sessions: List[String] = Nil
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   631
  ) {
66736
148891036469 more standard merge operation;
wenzelm
parents: 66722
diff changeset
   632
    def ++ (other: Selection): Selection =
65422
b606c98e6d10 tuned signature;
wenzelm
parents: 65420
diff changeset
   633
      Selection(
b606c98e6d10 tuned signature;
wenzelm
parents: 65420
diff changeset
   634
        requirements = requirements || other.requirements,
b606c98e6d10 tuned signature;
wenzelm
parents: 65420
diff changeset
   635
        all_sessions = all_sessions || other.all_sessions,
66737
2edc0c42c883 option -B for "isabelle build" and "isabelle imports";
wenzelm
parents: 66736
diff changeset
   636
        base_sessions = Library.merge(base_sessions, other.base_sessions),
66736
148891036469 more standard merge operation;
wenzelm
parents: 66722
diff changeset
   637
        exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
148891036469 more standard merge operation;
wenzelm
parents: 66722
diff changeset
   638
        exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
148891036469 more standard merge operation;
wenzelm
parents: 66722
diff changeset
   639
        session_groups = Library.merge(session_groups, other.session_groups),
148891036469 more standard merge operation;
wenzelm
parents: 66722
diff changeset
   640
        sessions = Library.merge(sessions, other.sessions))
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   641
  }
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   642
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   643
  object Structure {
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   644
    val empty: Structure = make(Chapter_Defs.empty, Nil)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72855
diff changeset
   645
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   646
    def make(chapter_defs: Chapter_Defs, infos: List[Info]): Structure = {
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   647
      def add_edges(
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   648
        graph: Graph[String, Info],
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   649
        kind: String,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   650
        edges: Info => Iterable[String]
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   651
      ) : Graph[String, Info] = {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   652
        def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = {
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   653
          if (!g.defined(parent))
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   654
            error("Bad " + kind + " session " + quote(parent) + " for " +
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   655
              quote(name) + Position.here(pos))
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   656
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   657
          try { g.add_edge_acyclic(parent, name) }
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   658
          catch {
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   659
            case exn: Graph.Cycles[_] =>
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   660
              error(cat_lines(exn.cycles.map(cycle =>
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   661
                "Cyclic session dependency of " +
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   662
                  cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   663
          }
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   664
        }
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   665
        graph.iterator.foldLeft(graph) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   666
          case (g, (name, (info, _))) =>
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   667
            edges(info).foldLeft(g)(add_edge(info.pos, name, _, _))
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   668
        }
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   669
      }
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   670
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   671
      val info_graph =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   672
        infos.foldLeft(Graph.string[Info]) {
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   673
          case (graph, info) =>
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   674
            if (graph.defined(info.name))
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   675
              error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   676
                Position.here(graph.get_node(info.name).pos))
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   677
            else graph.new_node(info.name, info)
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   678
        }
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   679
      val build_graph = add_edges(info_graph, "parent", _.parent)
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   680
      val imports_graph = add_edges(build_graph, "imports", _.imports)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   681
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   682
      val session_positions: List[(String, Position.T)] =
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   683
        (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   684
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   685
      val session_directories: Map[JFile, String] =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   686
        (for {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   687
          session <- imports_graph.topological_order.iterator
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   688
          info = info_graph.get_node(session)
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   689
          dir <- info.dirs.iterator
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   690
        } yield (info, dir)).foldLeft(Map.empty[JFile, String]) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   691
            case (dirs, (info, dir)) =>
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   692
              val session = info.name
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   693
              val canonical_dir = dir.canonical_file
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   694
              dirs.get(canonical_dir) match {
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   695
                case Some(session1) =>
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   696
                  val info1 = info_graph.get_node(session1)
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   697
                  error("Duplicate use of directory " + dir +
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   698
                    "\n  for session " + quote(session1) + Position.here(info1.pos) +
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   699
                    "\n  vs. session " + quote(session) + Position.here(info.pos))
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   700
                case None => dirs + (canonical_dir -> session)
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   701
              }
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   702
          }
70671
cb1776c8e216 clarified signature: retain global session information, unaffected by later restriction;
wenzelm
parents: 70668
diff changeset
   703
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   704
      val global_theories: Map[String, String] =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   705
        (for {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   706
          session <- imports_graph.topological_order.iterator
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   707
          info = info_graph.get_node(session)
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   708
          thy <- info.global_theories.iterator }
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   709
          yield (info, thy)).foldLeft(Thy_Header.bootstrap_global_theories.toMap) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   710
            case (global, (info, thy)) =>
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   711
              val qualifier = info.name
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   712
              global.get(thy) match {
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   713
                case Some(qualifier1) if qualifier != qualifier1 =>
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   714
                  error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   715
                case _ => global + (thy -> qualifier)
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   716
              }
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   717
          }
70671
cb1776c8e216 clarified signature: retain global session information, unaffected by later restriction;
wenzelm
parents: 70668
diff changeset
   718
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   719
      new Structure(chapter_defs, session_positions, session_directories,
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   720
        global_theories, build_graph, imports_graph)
72855
e0f6fa6ff3d0 tuned signature;
wenzelm
parents: 72854
diff changeset
   721
    }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   722
  }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   723
67052
caf87d4b9b61 tuned signature;
wenzelm
parents: 67029
diff changeset
   724
  final class Structure private[Sessions](
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   725
    val chapter_defs: Chapter_Defs,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   726
    val session_positions: List[(String, Position.T)],
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   727
    val session_directories: Map[JFile, String],
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   728
    val global_theories: Map[String, String],
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   729
    val build_graph: Graph[String, Info],
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   730
    val imports_graph: Graph[String, Info]
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   731
  ) {
69524
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   732
    sessions_structure =>
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   733
75885
8342cba8eae8 clarified signature: avoid constants from Sessions.Structure within Session.Base;
wenzelm
parents: 75884
diff changeset
   734
    def bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
72845
60f56f623be2 tuned signature;
wenzelm
parents: 72839
diff changeset
   735
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   736
    def dest_session_directories: List[(String, String)] =
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   737
      for ((file, session) <- session_directories.toList)
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   738
        yield (File.standard_path(file), session)
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   739
69762
58fb0d779583 support for session information via virtual file-system;
wenzelm
parents: 69671
diff changeset
   740
    lazy val chapters: SortedMap[String, List[Info]] =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   741
      build_graph.iterator.foldLeft(SortedMap.empty[String, List[Info]]) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   742
        case (chs, (_, (info, _))) =>
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   743
          chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil)))
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
   744
      }
69762
58fb0d779583 support for session information via virtual file-system;
wenzelm
parents: 69671
diff changeset
   745
66823
f529719cc47d operations for graph display;
wenzelm
parents: 66822
diff changeset
   746
    def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
f529719cc47d operations for graph display;
wenzelm
parents: 66822
diff changeset
   747
    def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
f529719cc47d operations for graph display;
wenzelm
parents: 66822
diff changeset
   748
67025
961285f581e6 clarifified selection: always wrt. build_graph structure;
wenzelm
parents: 67024
diff changeset
   749
    def defined(name: String): Boolean = imports_graph.defined(name)
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   750
    def apply(name: String): Info = imports_graph.get_node(name)
67025
961285f581e6 clarifified selection: always wrt. build_graph structure;
wenzelm
parents: 67024
diff changeset
   751
    def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   752
70859
6e6254bbce1f split into standard partitions, for improved scalability;
wenzelm
parents: 70796
diff changeset
   753
    def theory_qualifier(name: String): String =
6e6254bbce1f split into standard partitions, for improved scalability;
wenzelm
parents: 70796
diff changeset
   754
      global_theories.getOrElse(name, Long_Name.qualifier(name))
75884
3d8b37b1d798 clarified signature: avoid object-oriented HTML_Context;
wenzelm
parents: 75791
diff changeset
   755
    def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
70859
6e6254bbce1f split into standard partitions, for improved scalability;
wenzelm
parents: 70796
diff changeset
   756
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   757
    def check_sessions(names: List[String]): Unit = {
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71599
diff changeset
   758
      val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
68542
02df6c68a8cb clarified error;
wenzelm
parents: 68523
diff changeset
   759
      if (bad_sessions.nonEmpty)
02df6c68a8cb clarified error;
wenzelm
parents: 68523
diff changeset
   760
        error("Undefined session(s): " + commas_quote(bad_sessions))
02df6c68a8cb clarified error;
wenzelm
parents: 68523
diff changeset
   761
    }
02df6c68a8cb clarified error;
wenzelm
parents: 68523
diff changeset
   762
68733
76e339ef60e3 more uniform checks;
wenzelm
parents: 68732
diff changeset
   763
    def check_sessions(sel: Selection): Unit =
76e339ef60e3 more uniform checks;
wenzelm
parents: 68732
diff changeset
   764
      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
76e339ef60e3 more uniform checks;
wenzelm
parents: 68732
diff changeset
   765
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   766
    private def selected(graph: Graph[String, Info], sel: Selection): List[String] = {
68733
76e339ef60e3 more uniform checks;
wenzelm
parents: 68732
diff changeset
   767
      check_sessions(sel)
76e339ef60e3 more uniform checks;
wenzelm
parents: 68732
diff changeset
   768
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   769
      val select_group = sel.session_groups.toSet
68734
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68733
diff changeset
   770
      val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   771
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   772
      val selected0 =
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   773
        if (sel.all_sessions) graph.keys
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   774
        else {
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   775
          (for {
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   776
            (name, (info, _)) <- graph.iterator
74810
d540c36cd0d2 tuned (see also e0d1d9203275);
wenzelm
parents: 74809
diff changeset
   777
            if info.dir_selected || select_session(name) || info.groups.exists(select_group)
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   778
          } yield name).toList
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   779
        }
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   780
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   781
      if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   782
      else selected0
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   783
    }
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   784
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   785
    def selection(sel: Selection): Structure = {
68733
76e339ef60e3 more uniform checks;
wenzelm
parents: 68732
diff changeset
   786
      check_sessions(sel)
67025
961285f581e6 clarifified selection: always wrt. build_graph structure;
wenzelm
parents: 67024
diff changeset
   787
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   788
      val excluded = {
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   789
        val exclude_group = sel.exclude_session_groups.toSet
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   790
        val exclude_group_sessions =
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   791
          (for {
68734
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68733
diff changeset
   792
            (name, (info, _)) <- imports_graph.iterator
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68733
diff changeset
   793
            if imports_graph.get_node(name).groups.exists(exclude_group)
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   794
          } yield name).toList
68734
c14a2cc9b5ef isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents: 68733
diff changeset
   795
        imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   796
      }
67027
wenzelm
parents: 67026
diff changeset
   797
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   798
      def restrict(graph: Graph[String, Info]): Graph[String, Info] = {
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   799
        val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
67029
d6d9fd2559ce clarified signature (again);
wenzelm
parents: 67028
diff changeset
   800
        graph.restrict(graph.all_preds(sessions).toSet)
67025
961285f581e6 clarifified selection: always wrt. build_graph structure;
wenzelm
parents: 67024
diff changeset
   801
      }
961285f581e6 clarifified selection: always wrt. build_graph structure;
wenzelm
parents: 67024
diff changeset
   802
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   803
      new Structure(chapter_defs, session_positions, session_directories, global_theories,
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70681
diff changeset
   804
        restrict(build_graph), restrict(imports_graph))
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   805
    }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   806
72571
ab4a0b19648a tuned signature;
wenzelm
parents: 72565
diff changeset
   807
    def selection(session: String): Structure = selection(Selection.session(session))
ab4a0b19648a tuned signature;
wenzelm
parents: 72565
diff changeset
   808
69524
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   809
    def selection_deps(
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   810
      selection: Selection,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71642
diff changeset
   811
      progress: Progress = new Progress,
69524
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   812
      loading_sessions: Boolean = false,
68304
09270aa40884 tuned signature;
wenzelm
parents: 68294
diff changeset
   813
      inlined_files: Boolean = false,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   814
      verbose: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   815
    ): Deps = {
69524
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   816
      val deps =
70869
1d063b7f7928 incorporate sessions with record_proofs;
wenzelm
parents: 70867
diff changeset
   817
        Sessions.deps(sessions_structure.selection(selection),
69524
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   818
          progress = progress, inlined_files = inlined_files, verbose = verbose)
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   819
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   820
      if (loading_sessions) {
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   821
        val selection_size = deps.sessions_structure.build_graph.size
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   822
        if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   823
      }
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   824
fa94f2b2a877 clarified sessions_deps, according to Isabelle/MMT usage;
wenzelm
parents: 69393
diff changeset
   825
      deps
68304
09270aa40884 tuned signature;
wenzelm
parents: 68294
diff changeset
   826
    }
09270aa40884 tuned signature;
wenzelm
parents: 68294
diff changeset
   827
75760
f8be63d2ec6f more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
wenzelm
parents: 75759
diff changeset
   828
    def build_hierarchy(session: String): List[String] =
f8be63d2ec6f more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
wenzelm
parents: 75759
diff changeset
   829
      if (build_graph.defined(session)) build_graph.all_preds(List(session))
f8be63d2ec6f more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
wenzelm
parents: 75759
diff changeset
   830
      else List(session)
f8be63d2ec6f more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
wenzelm
parents: 75759
diff changeset
   831
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   832
    def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
67029
d6d9fd2559ce clarified signature (again);
wenzelm
parents: 67028
diff changeset
   833
    def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
72065
11dc8929832d clarified order --- proper sorting of requirements;
wenzelm
parents: 72064
diff changeset
   834
    def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
67029
d6d9fd2559ce clarified signature (again);
wenzelm
parents: 67028
diff changeset
   835
    def build_topological_order: List[String] = build_graph.topological_order
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   836
68732
5472f4409fe6 tuned signature;
wenzelm
parents: 68542
diff changeset
   837
    def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
67029
d6d9fd2559ce clarified signature (again);
wenzelm
parents: 67028
diff changeset
   838
    def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
72065
11dc8929832d clarified order --- proper sorting of requirements;
wenzelm
parents: 72064
diff changeset
   839
    def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
67029
d6d9fd2559ce clarified signature (again);
wenzelm
parents: 67028
diff changeset
   840
    def imports_topological_order: List[String] = imports_graph.topological_order
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   841
72613
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   842
    def bibtex_entries: List[(String, List[String])] =
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   843
      build_topological_order.flatMap(name =>
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   844
        apply(name).bibtex_entries match {
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   845
          case Nil => None
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   846
          case entries => Some(name -> entries.map(_.info))
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   847
        })
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72604
diff changeset
   848
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   849
    override def toString: String =
67052
caf87d4b9b61 tuned signature;
wenzelm
parents: 67029
diff changeset
   850
      imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   851
  }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   852
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   853
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   854
  /* parser */
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   855
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   856
  private val CHAPTER_DEFINITION = "chapter_definition"
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   857
  private val CHAPTER = "chapter"
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   858
  private val SESSION = "session"
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   859
  private val IN = "in"
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   860
  private val DESCRIPTION = "description"
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   861
  private val DIRECTORIES = "directories"
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   862
  private val OPTIONS = "options"
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   863
  private val SESSIONS = "sessions"
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   864
  private val THEORIES = "theories"
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65373
diff changeset
   865
  private val GLOBAL = "global"
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   866
  private val DOCUMENT_THEORIES = "document_theories"
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   867
  private val DOCUMENT_FILES = "document_files"
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   868
  private val EXPORT_FILES = "export_files"
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   869
  private val EXPORT_CLASSPATH = "export_classpath"
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   870
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71599
diff changeset
   871
  val root_syntax: Outer_Syntax =
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   872
    Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   873
      GLOBAL + IN +
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   874
      (CHAPTER_DEFINITION, Keyword.THY_DECL) +
63443
c037248d54e8 clarified keywords;
wenzelm
parents: 63022
diff changeset
   875
      (CHAPTER, Keyword.THY_DECL) +
c037248d54e8 clarified keywords;
wenzelm
parents: 63022
diff changeset
   876
      (SESSION, Keyword.THY_DECL) +
c037248d54e8 clarified keywords;
wenzelm
parents: 63022
diff changeset
   877
      (DESCRIPTION, Keyword.QUASI_COMMAND) +
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   878
      (DIRECTORIES, Keyword.QUASI_COMMAND) +
63443
c037248d54e8 clarified keywords;
wenzelm
parents: 63022
diff changeset
   879
      (OPTIONS, Keyword.QUASI_COMMAND) +
65420
695d4e22345a support for static session imports, without affect build hierarchy;
wenzelm
parents: 65419
diff changeset
   880
      (SESSIONS, Keyword.QUASI_COMMAND) +
63443
c037248d54e8 clarified keywords;
wenzelm
parents: 63022
diff changeset
   881
      (THEORIES, Keyword.QUASI_COMMAND) +
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   882
      (DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) +
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   883
      (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   884
      (EXPORT_FILES, Keyword.QUASI_COMMAND) +
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   885
      (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   886
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   887
  abstract class Entry
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   888
  sealed case class Chapter_Def(pos: Position.T, name: String, description: String) extends Entry
75984
75b65c1f7a1f tuned signature;
wenzelm
parents: 75978
diff changeset
   889
  sealed case class Chapter_Entry(name: String) extends Entry
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   890
  sealed case class Session_Entry(
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   891
    pos: Position.T,
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   892
    name: String,
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   893
    groups: List[String],
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   894
    path: String,
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   895
    parent: Option[String],
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   896
    description: String,
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   897
    options: List[Options.Spec],
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   898
    imports: List[String],
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   899
    directories: List[String],
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   900
    theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   901
    document_theories: List[(String, Position.T)],
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   902
    document_files: List[(String, String)],
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   903
    export_files: List[(String, Int, List[String])],
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   904
    export_classpath: List[String]
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   905
  ) extends Entry {
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   906
    def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   907
      theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
72666
945cee776e79 proper meta_digest: avoid non-portable position information;
wenzelm
parents: 72653
diff changeset
   908
    def document_theories_no_position: List[String] =
945cee776e79 proper meta_digest: avoid non-portable position information;
wenzelm
parents: 72653
diff changeset
   909
      document_theories.map(_._1)
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   910
  }
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
   911
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   912
  object Chapter_Defs {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   913
    val empty: Chapter_Defs = new Chapter_Defs(Nil)
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   914
  }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   915
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   916
  class Chapter_Defs private(rev_list: List[Chapter_Def]) {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   917
    def list: List[Chapter_Def] = rev_list.reverse
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   918
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   919
    override def toString: String =
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   920
      list.map(_.name).mkString("Chapter_Defs(", ", ", ")")
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   921
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   922
    private def find(chapter: String): Option[Chapter_Def] =
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   923
      rev_list.find(_.name == chapter)
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   924
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   925
    def apply(chapter: String): String =
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   926
      find(chapter) match {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   927
        case None => ""
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   928
        case Some(ch_def) => ch_def.description
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   929
      }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   930
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   931
    def + (ch_def: Chapter_Def): Chapter_Defs =
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   932
      if (ch_def.description.isEmpty) this
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   933
      else {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   934
        find(ch_def.name) match {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   935
          case None => new Chapter_Defs(ch_def :: rev_list)
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   936
          case Some(old_def) =>
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   937
            error("Duplicate chapter definition " + quote(ch_def.name) +
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   938
              Position.here(old_def.pos) + Position.here(ch_def.pos))
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   939
        }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   940
      }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   941
  }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   942
75405
b13ab7d11b90 clarified signature: avoid ambiguity in scala3;
wenzelm
parents: 75394
diff changeset
   943
  private object Parsers extends Options.Parsers {
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   944
    private val chapter_name: Parser[String] =
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   945
      atom("chapter name", _.is_name)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   946
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   947
    private val chapter_def: Parser[Chapter_Def] =
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   948
      command(CHAPTER_DEFINITION) ~!
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   949
        (position(chapter_name) ~ $$$(DESCRIPTION) ~ text) ^^
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   950
        { case _ ~ ((a, pos) ~ _ ~ b) => Chapter_Def(pos, a, b) }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   951
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
   952
    private val chapter_entry: Parser[Chapter_Entry] =
75984
75b65c1f7a1f tuned signature;
wenzelm
parents: 75978
diff changeset
   953
      command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   954
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   955
    private val session_entry: Parser[Session_Entry] = {
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   956
      val option =
67210
wenzelm
parents: 67097
diff changeset
   957
        option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
wenzelm
parents: 67097
diff changeset
   958
          { case x ~ y => (x, y) }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   959
      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   960
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65373
diff changeset
   961
      val theory_entry =
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 70650
diff changeset
   962
        position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65373
diff changeset
   963
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   964
      val theories =
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65373
diff changeset
   965
        $$$(THEORIES) ~!
66970
13857f49d215 clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
wenzelm
parents: 66969
diff changeset
   966
          ((options | success(Nil)) ~ rep1(theory_entry)) ^^
65374
a5b38d8d3c1e tuned syntax;
wenzelm
parents: 65373
diff changeset
   967
          { case _ ~ (x ~ y) => (x, y) }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   968
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   969
      val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   970
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   971
      val document_theories =
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   972
        $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x }
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   973
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   974
      val document_files =
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   975
        $$$(DOCUMENT_FILES) ~!
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   976
          ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   977
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69560
diff changeset
   978
      val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
2486792eaf61 support pruning of export names;
wenzelm
parents: 69560
diff changeset
   979
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
   980
      val export_files =
69671
2486792eaf61 support pruning of export names;
wenzelm
parents: 69560
diff changeset
   981
        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
2486792eaf61 support pruning of export names;
wenzelm
parents: 69560
diff changeset
   982
          { case _ ~ (x ~ y ~ z) => (x, y, z) }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   983
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   984
      val export_classpath =
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   985
        $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   986
          { case _ ~ x => x }
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
   987
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   988
      command(SESSION) ~!
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   989
        (position(session_name) ~
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   990
          (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   991
          (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   992
          ($$$("=") ~!
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   993
            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   994
              (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
   995
              (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
66970
13857f49d215 clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
wenzelm
parents: 66969
diff changeset
   996
              (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70679
diff changeset
   997
              (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
66970
13857f49d215 clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
wenzelm
parents: 66969
diff changeset
   998
              rep(theories) ~
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72574
diff changeset
   999
              (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68221
diff changeset
  1000
              (rep(document_files) ^^ (x => x.flatten)) ~
75679
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
  1001
              rep(export_files) ~
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
  1002
              opt(export_classpath)))) ^^
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
  1003
        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l ~ m))) =>
aa89255b704c support for classpath artifacts within session structure:
wenzelm
parents: 75672
diff changeset
  1004
            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l, m.getOrElse(Nil)) }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1005
    }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1006
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1007
    def parse_root(path: Path): List[Entry] = {
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1008
      val toks = Token.explode(root_syntax.keywords, File.read(path))
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1009
      val start = Token.Pos.file(path.implode)
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1010
      val parser: Parser[Entry] = chapter_def | chapter_entry | session_entry
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1011
      parse_all(rep(parser), Token.reader(toks, start)) match {
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1012
        case Success(result, _) => result
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1013
        case bad => error(bad.toString)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1014
      }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1015
    }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1016
  }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1017
75405
b13ab7d11b90 clarified signature: avoid ambiguity in scala3;
wenzelm
parents: 75394
diff changeset
  1018
  def parse_root(path: Path): List[Entry] = Parsers.parse_root(path)
66819
wenzelm
parents: 66818
diff changeset
  1019
wenzelm
parents: 66818
diff changeset
  1020
  def parse_root_entries(path: Path): List[Session_Entry] =
75405
b13ab7d11b90 clarified signature: avoid ambiguity in scala3;
wenzelm
parents: 75394
diff changeset
  1021
    for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
66819
wenzelm
parents: 66818
diff changeset
  1022
    yield entry.asInstanceOf[Session_Entry]
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1023
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1024
  def read_root(
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1025
    options: Options,
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1026
    select: Boolean,
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1027
    path: Path,
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1028
    chapter_defs: Chapter_Defs
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1029
  ): (List[Info], Chapter_Defs) = {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1030
    var chapter_defs1 = chapter_defs
69762
58fb0d779583 support for session information via virtual file-system;
wenzelm
parents: 69671
diff changeset
  1031
    var entry_chapter = UNSORTED
66960
d62f1f03868a tuned signature;
wenzelm
parents: 66959
diff changeset
  1032
    val infos = new mutable.ListBuffer[Info]
66819
wenzelm
parents: 66818
diff changeset
  1033
    parse_root(path).foreach {
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1034
      case ch_def: Chapter_Def => chapter_defs1 += ch_def
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1035
      case entry: Chapter_Entry => entry_chapter = entry.name
66967
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
  1036
      case entry: Session_Entry =>
e365c91c72a9 synthesize session with all required theories from other session imports;
wenzelm
parents: 66966
diff changeset
  1037
        infos += make_info(options, select, path.dir, entry_chapter, entry)
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1038
    }
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1039
    (infos.toList, chapter_defs1)
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1040
  }
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1041
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1042
  def parse_roots(roots: Path): List[String] = {
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1043
    for {
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1044
      line <- split_lines(File.read(roots))
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1045
      if !(line == "" || line.startsWith("#"))
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1046
    } yield line
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1047
  }
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1048
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1049
62635
4854a38061de tuned signature;
wenzelm
parents: 62633
diff changeset
  1050
  /* load sessions from certain directories */
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1051
73814
c8b4a4f69068 clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);
wenzelm
parents: 73718
diff changeset
  1052
  def is_session_dir(dir: Path): Boolean =
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1053
    (dir + ROOT).is_file || (dir + ROOTS).is_file
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1054
75297
fc4d07587695 more robust errors -- on foreground process instead of background server;
wenzelm
parents: 74812
diff changeset
  1055
  def check_session_dir(dir: Path): Path =
65468
c41791ad75c3 early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;
wenzelm
parents: 65463
diff changeset
  1056
    if (is_session_dir(dir)) File.pwd() + dir.expand
73311
54262af6d310 clarified message;
wenzelm
parents: 73310
diff changeset
  1057
    else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1058
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1059
  def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {
73815
43882e34c038 clarified modules;
wenzelm
parents: 73814
diff changeset
  1060
    val default_dirs = Components.directories().filter(is_session_dir)
68746
f95e2f145ea5 canonical session directories in correspondence to Known.files;
wenzelm
parents: 68734
diff changeset
  1061
    for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
f95e2f145ea5 canonical session directories in correspondence to Known.files;
wenzelm
parents: 68734
diff changeset
  1062
    yield (select, dir.canonical)
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65560
diff changeset
  1063
  }
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65560
diff changeset
  1064
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1065
  def load_structure(
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1066
    options: Options,
66968
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
  1067
    dirs: List[Path] = Nil,
9991671c98aa allow to augment session context via explicit session infos;
wenzelm
parents: 66967
diff changeset
  1068
    select_dirs: List[Path] = Nil,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1069
    infos: List[Info] = Nil
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1070
  ): Structure = {
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1071
    def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
62635
4854a38061de tuned signature;
wenzelm
parents: 62633
diff changeset
  1072
      load_root(select, dir) ::: load_roots(select, dir)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1073
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1074
    def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = {
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1075
      val root = dir + ROOT
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1076
      if (root.is_file) List((select, root)) else Nil
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1077
    }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1078
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1079
    def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = {
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1080
      val roots = dir + ROOTS
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1081
      if (roots.is_file) {
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1082
        for {
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1083
          entry <- parse_roots(roots)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1084
          dir1 =
66818
5bc903a60932 clarified signature: public access to ROOT file syntax;
wenzelm
parents: 66780
diff changeset
  1085
            try { check_session_dir(dir + Path.explode(entry)) }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1086
            catch {
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1087
              case ERROR(msg) =>
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1088
                error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1089
            }
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1090
          res <- load_dir(select, dir1)
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1091
        } yield res
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1092
      }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1093
      else Nil
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1094
    }
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1095
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1096
    val roots =
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1097
      for {
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65560
diff changeset
  1098
        (select, dir) <- directories(dirs, select_dirs)
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1099
        res <- load_dir(select, check_session_dir(dir))
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1100
      } yield res
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1101
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1102
    val unique_roots =
73359
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1103
      roots.foldLeft(Map.empty[JFile, (Boolean, Path)]) {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1104
        case (m, (select, path)) =>
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1105
          val file = path.canonical_file
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1106
          m.get(file) match {
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1107
            case None => m + (file -> (select, path))
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1108
            case Some((select1, path1)) => m + (file -> (select1 || select, path1))
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1109
          }
d8a0e996614b tuned --- fewer warnings;
wenzelm
parents: 73357
diff changeset
  1110
      }.toList.map(_._2)
66764
006deaf5c3dc process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents: 66759
diff changeset
  1111
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1112
    val (chapter_defs, info_roots) = {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1113
      var chapter_defs = Chapter_Defs.empty
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1114
      val result = new mutable.ListBuffer[Info]
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1115
      for { (select, path) <- unique_roots } {
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1116
        val (infos, chapter_defs1) = read_root(options, select, path, chapter_defs)
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1117
        chapter_defs = chapter_defs1
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1118
        result ++= infos
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1119
      }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1120
      (chapter_defs, result.toList)
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1121
    }
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1122
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 75984
diff changeset
  1123
    Structure.make(chapter_defs, info_roots ::: infos)
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1124
  }
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1125
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1126
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1127
  /* Isabelle tool wrapper */
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1128
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72760
diff changeset
  1129
  val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1130
    Scala_Project.here,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1131
    { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1132
      var base_sessions: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1133
      var select_dirs: List[Path] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1134
      var requirements = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1135
      var exclude_session_groups: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1136
      var all_sessions = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1137
      var dirs: List[Path] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1138
      var session_groups: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1139
      var exclude_sessions: List[String] = Nil
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1140
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1141
      val getopts = Getopts("""
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1142
Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1143
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1144
  Options are:
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1145
    -B NAME      include session NAME and all descendants
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1146
    -D DIR       include session directory and select its sessions
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1147
    -R           refer to requirements of selected sessions
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1148
    -X NAME      exclude sessions from group NAME and all descendants
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1149
    -a           select all sessions
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1150
    -d DIR       include session directory
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1151
    -g NAME      select session group NAME
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1152
    -x NAME      exclude session NAME and all descendants
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1153
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1154
  Explore the structure of Isabelle sessions and print result names in
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1155
  topological order (on stdout).
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1156
""",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1157
        "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1158
        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1159
        "R" -> (_ => requirements = true),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1160
        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1161
        "a" -> (_ => all_sessions = true),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1162
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1163
        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1164
        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1165
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1166
      val sessions = getopts(args)
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1167
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1168
      val options = Options.init()
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1169
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1170
      val selection =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1171
        Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1172
          exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1173
          session_groups = session_groups, sessions = sessions)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1174
      val sessions_structure =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1175
        load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1176
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1177
      for (name <- sessions_structure.imports_topological_order) {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1178
        Output.writeln(name, stdout = true)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1179
      }
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1180
    })
71808
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1181
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71726
diff changeset
  1182
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62636
diff changeset
  1183
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1184
  /** heap file with SHA1 digest **/
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1185
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1186
  private val sha1_prefix = "SHA1:"
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1187
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1188
  def read_heap_digest(heap: Path): Option[String] = {
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1189
    if (heap.is_file) {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1190
      using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1191
        val len = file.size
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1192
        val n = sha1_prefix.length + SHA1.digest_length
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1193
        if (len >= n) {
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1194
          file.position(len - n)
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1195
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1196
          val buf = ByteBuffer.allocate(n)
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1197
          var i = 0
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1198
          var m = 0
75709
a068fb7346ef clarified while-loops;
wenzelm
parents: 75680
diff changeset
  1199
          while ({
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1200
            m = file.read(buf)
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1201
            if (m != -1) i += m
75709
a068fb7346ef clarified while-loops;
wenzelm
parents: 75680
diff changeset
  1202
            m != -1 && n > i
a068fb7346ef clarified while-loops;
wenzelm
parents: 75680
diff changeset
  1203
          }) ()
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1204
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1205
          if (i == n) {
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1206
            val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1207
            val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1208
            if (prefix == sha1_prefix) Some(s) else None
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1209
          }
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1210
          else None
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1211
        }
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1212
        else None
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1213
      }
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1214
    }
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1215
    else None
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1216
  }
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1217
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1218
  def write_heap_digest(heap: Path): String =
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1219
    read_heap_digest(heap) match {
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1220
      case None =>
75310
42baf7ffa088 tuned signature;
wenzelm
parents: 75297
diff changeset
  1221
        val s = SHA1.digest(heap).toString
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1222
        File.append(heap, sha1_prefix + s)
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1223
        s
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1224
      case Some(s) => s
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1225
    }
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1226
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1227
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62637
diff changeset
  1228
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62636
diff changeset
  1229
  /** persistent store **/
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1230
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1231
  object Session_Info {
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66848
diff changeset
  1232
    val session_name = SQL.Column.string("session_name").make_primary_key
65326
cb7cb57c7ce1 proper primary key;
wenzelm
parents: 65324
diff changeset
  1233
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1234
    // Build_Log.Session_Info
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1235
    val session_timing = SQL.Column.bytes("session_timing")
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1236
    val command_timings = SQL.Column.bytes("command_timings")
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1237
    val theory_timings = SQL.Column.bytes("theory_timings")
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1238
    val ml_statistics = SQL.Column.bytes("ml_statistics")
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1239
    val task_statistics = SQL.Column.bytes("task_statistics")
65934
5f202ba9f590 store errors in build db;
wenzelm
parents: 65857
diff changeset
  1240
    val errors = SQL.Column.bytes("errors")
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1241
    val build_log_columns =
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1242
      List(session_name, session_timing, command_timings, theory_timings,
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1243
        ml_statistics, task_statistics, errors)
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1244
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1245
    // Build.Session_Info
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1246
    val sources = SQL.Column.string("sources")
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1247
    val input_heaps = SQL.Column.string("input_heaps")
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1248
    val output_heap = SQL.Column.string("output_heap")
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1249
    val return_code = SQL.Column.int("return_code")
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1250
    val uuid = SQL.Column.string("uuid")
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1251
    val build_columns = List(sources, input_heaps, output_heap, return_code, uuid)
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1252
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1253
    val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1254
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1255
    val augment_table: PostgreSQL.Source =
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1256
      "ALTER TABLE IF EXISTS " + table.ident +
75978
0b4944b25b9d tuned whitespace;
wenzelm
parents: 75977
diff changeset
  1257
      " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1258
  }
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1259
74731
161e84e6b40a just one cache, via HTML_Context, via Sessions.Store or Session;
wenzelm
parents: 74696
diff changeset
  1260
  def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
73031
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1261
    new Store(options, cache)
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1262
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1263
  class Store private[Sessions](val options: Options, val cache: Term.Cache) {
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1264
    store =>
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1265
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1266
    override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
68219
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1267
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1268
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1269
    /* directories */
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1270
68523
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68483
diff changeset
  1271
    val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
ccacc84e0251 clarified settings -- avoid hard-wired directories;
wenzelm
parents: 68483
diff changeset
  1272
    val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
68219
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1273
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1274
    def system_heaps: Boolean = options.bool("system_heaps")
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1275
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1276
    val output_dir: Path =
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1277
      if (system_heaps) system_output_dir else user_output_dir
68219
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1278
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1279
    val input_dirs: List[Path] =
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1280
      if (system_heaps) List(system_output_dir)
68219
c0341c0080e2 clarified store directories;
wenzelm
parents: 68218
diff changeset
  1281
      else List(user_output_dir, system_output_dir)
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1282
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72647
diff changeset
  1283
    def presentation_dir: Path =
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1284
      if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1285
      else Path.explode("$ISABELLE_BROWSER_INFO")
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1286
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62636
diff changeset
  1287
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1288
    /* file names */
65298
wenzelm
parents: 65297
diff changeset
  1289
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1290
    def heap(name: String): Path = Path.basic(name)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1291
    def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1292
    def log(name: String): Path = Path.basic("log") + Path.basic(name)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1293
    def log_gz(name: String): Path = log(name).ext("gz")
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62636
diff changeset
  1294
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1295
    def output_heap(name: String): Path = output_dir + heap(name)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1296
    def output_database(name: String): Path = output_dir + database(name)
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1297
    def output_log(name: String): Path = output_dir + log(name)
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1298
    def output_log_gz(name: String): Path = output_dir + log_gz(name)
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1299
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73311
diff changeset
  1300
    def prepare_output_dir(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
68220
8fc4e3d1df86 clarified store.clean_output: cleanup user_output_dir even in system_mode;
wenzelm
parents: 68219
diff changeset
  1301
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62636
diff changeset
  1302
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1303
    /* heap */
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62636
diff changeset
  1304
68212
5a59fded83c7 clarified heap vs. database operations: discontinued correlation of directory;
wenzelm
parents: 68210
diff changeset
  1305
    def find_heap(name: String): Option[Path] =
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1306
      input_dirs.map(_ + heap(name)).find(_.is_file)
68212
5a59fded83c7 clarified heap vs. database operations: discontinued correlation of directory;
wenzelm
parents: 68210
diff changeset
  1307
5a59fded83c7 clarified heap vs. database operations: discontinued correlation of directory;
wenzelm
parents: 68210
diff changeset
  1308
    def find_heap_digest(name: String): Option[String] =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71599
diff changeset
  1309
      find_heap(name).flatMap(read_heap_digest)
62632
cd991ba01ffd clarified modules;
wenzelm
parents: 62631
diff changeset
  1310
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1311
    def the_heap(name: String): Path =
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1312
      find_heap(name) getOrElse
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1313
        error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1314
          cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1315
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1316
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1317
    /* database */
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1318
75552
4aa3da02fd4d sync session images, based on accidental local state;
wenzelm
parents: 75406
diff changeset
  1319
    def find_database(name: String): Option[Path] =
4aa3da02fd4d sync session images, based on accidental local state;
wenzelm
parents: 75406
diff changeset
  1320
      input_dirs.map(_ + database(name)).find(_.is_file)
4aa3da02fd4d sync session images, based on accidental local state;
wenzelm
parents: 75406
diff changeset
  1321
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1322
    def database_server: Boolean = options.bool("build_database_server")
65281
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1323
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1324
    def open_database_server(): SQL.Database =
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1325
      PostgreSQL.open_database(
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1326
        user = options.string("build_database_user"),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1327
        password = options.string("build_database_password"),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1328
        database = options.string("build_database_name"),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1329
        host = options.string("build_database_host"),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1330
        port = options.int("build_database_port"),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1331
        ssh =
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1332
          options.proper_string("build_database_ssh_host").map(ssh_host =>
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1333
            SSH.open_session(options,
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1334
              host = ssh_host,
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1335
              user = options.string("build_database_ssh_user"),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1336
              port = options.int("build_database_ssh_port"))),
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1337
        ssh_close = true)
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1338
75775
70a65ee4a738 clarified signature: more robust treatment of server;
wenzelm
parents: 75774
diff changeset
  1339
    def try_open_database(
70a65ee4a738 clarified signature: more robust treatment of server;
wenzelm
parents: 75774
diff changeset
  1340
      name: String,
70a65ee4a738 clarified signature: more robust treatment of server;
wenzelm
parents: 75774
diff changeset
  1341
      output: Boolean = false,
70a65ee4a738 clarified signature: more robust treatment of server;
wenzelm
parents: 75774
diff changeset
  1342
      server: Boolean = database_server
70a65ee4a738 clarified signature: more robust treatment of server;
wenzelm
parents: 75774
diff changeset
  1343
    ): Option[SQL.Database] = {
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1344
      def check(db: SQL.Database): Option[SQL.Database] =
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73364
diff changeset
  1345
        if (output || session_info_exists(db)) Some(db) else { db.close(); None }
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1346
75775
70a65ee4a738 clarified signature: more robust treatment of server;
wenzelm
parents: 75774
diff changeset
  1347
      if (server) check(open_database_server())
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1348
      else if (output) Some(SQLite.open_database(output_database(name)))
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1349
      else {
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1350
        (for {
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1351
          dir <- input_dirs.view
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1352
          path = dir + database(name) if path.is_file
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1353
          db <- check(SQLite.open_database(path))
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1354
        } yield db).headOption
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1355
      }
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1356
    }
68212
5a59fded83c7 clarified heap vs. database operations: discontinued correlation of directory;
wenzelm
parents: 68210
diff changeset
  1357
75791
fb12433208aa tuned signature;
wenzelm
parents: 75786
diff changeset
  1358
    def error_database(name: String): Nothing =
75759
0cdccd0d1699 clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents: 75750
diff changeset
  1359
      error("Missing build database for session " + quote(name))
0cdccd0d1699 clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents: 75750
diff changeset
  1360
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1361
    def open_database(name: String, output: Boolean = false): SQL.Database =
75791
fb12433208aa tuned signature;
wenzelm
parents: 75786
diff changeset
  1362
      try_open_database(name, output = output) getOrElse error_database(name)
75759
0cdccd0d1699 clarified context for retrieval: more explicit types, with optional close() operation;
wenzelm
parents: 75750
diff changeset
  1363
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1364
    def clean_output(name: String): (Boolean, Boolean) = {
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1365
      val relevant_db =
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1366
        database_server && {
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1367
          try_open_database(name) match {
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1368
            case Some(db) =>
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1369
              try {
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1370
                db.transaction {
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1371
                  val relevant_db = session_info_defined(db, name)
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1372
                  init_session_info(db, name)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1373
                  relevant_db
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1374
                }
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73364
diff changeset
  1375
              } finally { db.close() }
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1376
            case None => false
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1377
          }
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1378
        }
68212
5a59fded83c7 clarified heap vs. database operations: discontinued correlation of directory;
wenzelm
parents: 68210
diff changeset
  1379
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1380
      val del =
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1381
        for {
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1382
          dir <-
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69812
diff changeset
  1383
            (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1384
          file <- List(heap(name), database(name), log(name), log_gz(name))
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1385
          path = dir + file if path.is_file
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1386
        } yield path.file.delete
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1387
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1388
      val relevant = relevant_db || del.nonEmpty
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1389
      val ok = del.forall(b => b)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1390
      (relevant, ok)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1391
    }
65287
75999f2a0c38 tuned message;
wenzelm
parents: 65286
diff changeset
  1392
75999f2a0c38 tuned message;
wenzelm
parents: 65286
diff changeset
  1393
68218
wenzelm
parents: 68217
diff changeset
  1394
    /* SQL database content */
wenzelm
parents: 68217
diff changeset
  1395
wenzelm
parents: 68217
diff changeset
  1396
    def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
wenzelm
parents: 68217
diff changeset
  1397
      db.using_statement(Session_Info.table.select(List(column),
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1398
        Session_Info.session_name.where_equal(name))) { stmt =>
68218
wenzelm
parents: 68217
diff changeset
  1399
        val res = stmt.execute_query()
wenzelm
parents: 68217
diff changeset
  1400
        if (!res.next()) Bytes.empty else res.bytes(column)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1401
      }
68218
wenzelm
parents: 68217
diff changeset
  1402
wenzelm
parents: 68217
diff changeset
  1403
    def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
73031
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1404
      Properties.uncompress(read_bytes(db, name, column), cache = cache)
68218
wenzelm
parents: 68217
diff changeset
  1405
wenzelm
parents: 68217
diff changeset
  1406
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1407
    /* session info */
65281
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1408
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1409
    def init_session_info(db: SQL.Database, name: String): Unit = {
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1410
      db.transaction {
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1411
        db.create_table(Session_Info.table)
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1412
        db.using_statement(
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73364
diff changeset
  1413
          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1414
        if (db.isInstanceOf[PostgreSQL.Database]) {
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1415
          db.using_statement(Session_Info.augment_table)(_.execute())
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1416
        }
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1417
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1418
        db.create_table(Export.Data.table)
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1419
        db.using_statement(
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73364
diff changeset
  1420
          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
  1421
73718
ecb31c3bf980 clarified modules;
wenzelm
parents: 73701
diff changeset
  1422
        db.create_table(Document_Build.Data.table)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
  1423
        db.using_statement(
73718
ecb31c3bf980 clarified modules;
wenzelm
parents: 73701
diff changeset
  1424
          Document_Build.Data.table.delete(
ecb31c3bf980 clarified modules;
wenzelm
parents: 73701
diff changeset
  1425
            Document_Build.Data.session_name.where_equal(name)))(_.execute())
68221
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1426
      }
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1427
    }
dbef88c2b6c5 support for build_database_server (PostgreSQL);
wenzelm
parents: 68220
diff changeset
  1428
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1429
    def session_info_exists(db: SQL.Database): Boolean = {
72634
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1430
      val tables = db.tables
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1431
      tables.contains(Session_Info.table.name) &&
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1432
      tables.contains(Export.Data.table.name)
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1433
    }
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1434
5cea0993ee4f clarified access to single database server vs. collection of database files;
wenzelm
parents: 72627
diff changeset
  1435
    def session_info_defined(db: SQL.Database, name: String): Boolean =
75739
5b37466c1463 removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents: 75738
diff changeset
  1436
      session_info_exists(db) && {
5b37466c1463 removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents: 75738
diff changeset
  1437
        db.using_statement(
5b37466c1463 removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents: 75738
diff changeset
  1438
          Session_Info.table.select(List(Session_Info.session_name),
5b37466c1463 removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
wenzelm
parents: 75738
diff changeset
  1439
            Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
68086
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1440
      }
9e1c670301b8 cleanup session output before starting build job;
wenzelm
parents: 68018
diff changeset
  1441
65296
a71db30f3b2d tuned signature;
wenzelm
parents: 65295
diff changeset
  1442
    def write_session_info(
65318
342efc382558 eliminated somewhat redundant inlined name (despite a7aa17a1f721);
wenzelm
parents: 65298
diff changeset
  1443
      db: SQL.Database,
65320
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1444
      name: String,
65318
342efc382558 eliminated somewhat redundant inlined name (despite a7aa17a1f721);
wenzelm
parents: 65298
diff changeset
  1445
      build_log: Build_Log.Session_Info,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1446
      build: Build.Session_Info
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1447
    ): Unit = {
65281
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1448
      db.transaction {
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1449
        val table = Session_Info.table
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1450
        db.using_statement(table.insert()) { stmt =>
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65740
diff changeset
  1451
          stmt.string(1) = name
65857
5d29d93766ef clarified use of XML.Cache;
wenzelm
parents: 65833
diff changeset
  1452
          stmt.bytes(2) = Properties.encode(build_log.session_timing)
73031
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1453
          stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1454
          stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.xz)
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1455
          stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.xz)
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1456
          stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.xz)
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1457
          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.xz)
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1458
          stmt.string(8) = build.sources
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1459
          stmt.string(9) = cat_lines(build.input_heaps)
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1460
          stmt.string(10) = build.output_heap getOrElse ""
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1461
          stmt.int(11) = build.return_code
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1462
          stmt.string(12) = build.uuid
65281
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1463
          stmt.execute()
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1464
        }
65281
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1465
      }
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1466
    }
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1467
65320
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1468
    def read_session_timing(db: SQL.Database, name: String): Properties.T =
73031
f93f0597f4fb clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents: 73024
diff changeset
  1469
      Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
65286
b661543a0de6 clarified signature;
wenzelm
parents: 65285
diff changeset
  1470
65320
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1471
    def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1472
      read_properties(db, name, Session_Info.command_timings)
65286
b661543a0de6 clarified signature;
wenzelm
parents: 65285
diff changeset
  1473
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1474
    def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1475
      read_properties(db, name, Session_Info.theory_timings)
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66857
diff changeset
  1476
65320
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1477
    def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1478
      read_properties(db, name, Session_Info.ml_statistics)
65286
b661543a0de6 clarified signature;
wenzelm
parents: 65285
diff changeset
  1479
65320
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1480
    def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
52861eebf58d access table via session_name: db may in principle contain multiple entries;
wenzelm
parents: 65318
diff changeset
  1481
      read_properties(db, name, Session_Info.task_statistics)
65286
b661543a0de6 clarified signature;
wenzelm
parents: 65285
diff changeset
  1482
72738
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72716
diff changeset
  1483
    def read_theories(db: SQL.Database, name: String): List[String] =
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72716
diff changeset
  1484
      read_theory_timings(db, name).flatMap(Markup.Name.unapply)
a4d7da18ac5c store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents: 72716
diff changeset
  1485
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
  1486
    def read_errors(db: SQL.Database, name: String): List[String] =
73033
d2690444c00a clarified caching;
wenzelm
parents: 73031
diff changeset
  1487
      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
  1488
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1489
    def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = {
66957
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1490
      if (db.tables.contains(Session_Info.table.name)) {
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1491
        db.using_statement(Session_Info.table.select(Nil,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1492
          Session_Info.session_name.where_equal(name))) { stmt =>
66957
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1493
          val res = stmt.execute_query()
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1494
          if (!res.next()) None
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1495
          else {
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1496
            val uuid =
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1497
              try { Option(res.string(Session_Info.uuid)).getOrElse("") }
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1498
              catch { case _: SQLException => "" }
66957
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1499
            Some(
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1500
              Build.Session_Info(
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1501
                res.string(Session_Info.sources),
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1502
                split_lines(res.string(Session_Info.input_heaps)),
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1503
                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
75967
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1504
                res.int(Session_Info.return_code),
ff164add75cd maintain "uuid" column in session build database, to identity the original build process uniquely;
wenzelm
parents: 75923
diff changeset
  1505
                uuid))
66957
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1506
          }
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1507
        }
66957
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1508
      }
82d13ba817b2 more permissive: db could be empty after hard crash;
wenzelm
parents: 66914
diff changeset
  1509
      else None
66744
fec1504e5f03 persistent storage of imported_sources;
wenzelm
parents: 66743
diff changeset
  1510
    }
65281
c70e7d24a16d SQL database operations for combined session info;
wenzelm
parents: 65278
diff changeset
  1511
  }
62631
c39614ddb80b clarified modules;
wenzelm
parents:
diff changeset
  1512
}