# HG changeset patch
# User wenzelm
# Date 1672844806 -3600
# Node ID e6f324723308c44d316f64ff6e1233640e71b12d
# Parent  4ef86dfe2296f8c0dcfe09231ce27c9e0b94e40f
clarified signature: more operations;

diff -r 4ef86dfe2296 -r e6f324723308 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Jan 04 15:53:36 2023 +0100
+++ b/src/Pure/Thy/export.scala	Wed Jan 04 16:06:46 2023 +0100
@@ -423,6 +423,14 @@
     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] = {
+      val store = database_context.store
+      (for {
+        database <- db_hierarchy.iterator
+        file <- store.read_sources(database.db, database.session, name = name).iterator
+      } yield file).nextOption()
+    }
+
     def node_source(name: Document.Node.Name): String = {
       def snapshot_source: Option[String] =
         for {
@@ -431,12 +439,8 @@
           text = node.source if text.nonEmpty
         } yield text
 
-      val store = database_context.store
       def db_source: Option[String] =
-        (for {
-          database <- db_hierarchy.iterator
-          file <- store.read_sources(database.db, database.session, name = name.node).iterator
-        } yield file.text).nextOption()
+        read_file(name.node).map(_.text)
 
       snapshot_source orElse db_source getOrElse ""
     }