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