--- a/src/Pure/Thy/sessions.scala Wed Aug 03 11:43:14 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Wed Aug 03 12:10:52 2022 +0200
@@ -71,7 +71,7 @@
known_loaded_files: Map[String, List[Path]] = Map.empty,
overall_syntax: Outer_Syntax = Outer_Syntax.empty,
imported_sources: List[(Path, SHA1.Digest)] = Nil,
- sources: List[(Path, SHA1.Digest)] = Nil,
+ session_sources: List[(Path, SHA1.Digest)] = Nil,
session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
errors: List[String] = Nil
) {
@@ -108,8 +108,8 @@
def imported_sources(name: String): List[SHA1.Digest] =
session_bases(name).imported_sources.map(_._2)
- def sources(name: String): List[SHA1.Digest] =
- session_bases(name).sources.map(_._2)
+ def session_sources(name: String): List[SHA1.Digest] =
+ session_bases(name).session_sources.map(_._2)
def errors: List[String] =
(for {
@@ -338,7 +338,7 @@
known_loaded_files = known_loaded_files,
overall_syntax = overall_syntax,
imported_sources = check_sources(imported_files),
- sources = check_sources(session_files),
+ session_sources = check_sources(session_files),
session_graph_display = session_graph_display,
errors = dependencies.errors ::: load_commands_errors ::: import_errors :::
document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
--- a/src/Pure/Tools/build.scala Wed Aug 03 11:43:14 2022 +0200
+++ b/src/Pure/Tools/build.scala Wed Aug 03 12:10:52 2022 +0200
@@ -203,7 +203,7 @@
def sources_stamp(deps: Sessions.Deps, session_name: String): String = {
val digests =
full_sessions(session_name).meta_digest ::
- deps.sources(session_name) :::
+ deps.session_sources(session_name) :::
deps.imported_sources(session_name)
SHA1.digest_set(digests).toString
}
@@ -247,7 +247,7 @@
val source_files =
(for {
(_, base) <- deps.session_bases.iterator
- (path, _) <- base.sources.iterator
+ (path, _) <- base.session_sources.iterator
} yield path).toList
val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
val unknown_files =