# HG changeset patch
# User wenzelm
# Date 1672846802 -3600
# Node ID c27fcf4a74955f5bcd36f95897d735ab5fc4f3a8
# Parent  e6f324723308c44d316f64ff6e1233640e71b12d
clarified signature: more operations;

diff -r e6f324723308 -r c27fcf4a7495 src/Pure/Thy/export.scala
--- 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] = {