--- a/src/Pure/Thy/export.scala Wed Jan 04 16:06:46 2023 +0100
+++ b/src/Pure/Thy/export.scala Wed Jan 04 16:40:02 2023 +0100
@@ -423,7 +423,7 @@
def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context =
new Theory_Context(session_context, theory, other_cache)
- def read_file(name: String): Option[Sessions.Source_File] = {
+ def get_source_file(name: String): Option[Sessions.Source_File] = {
val store = database_context.store
(for {
database <- db_hierarchy.iterator
@@ -431,6 +431,9 @@
} yield file).nextOption()
}
+ def source_file(name: String): Sessions.Source_File =
+ get_source_file(name).getOrElse(error("Missing session source file " + quote(name)))
+
def node_source(name: Document.Node.Name): String = {
def snapshot_source: Option[String] =
for {
@@ -439,10 +442,13 @@
text = node.source if text.nonEmpty
} yield text
- def db_source: Option[String] =
- read_file(name.node).map(_.text)
+ def db_source: String =
+ get_source_file(name.node) match {
+ case Some(file) => file.text
+ case None => ""
+ }
- snapshot_source orElse db_source getOrElse ""
+ snapshot_source getOrElse db_source
}
def classpath(): List[File.Content] = {