# HG changeset patch
# User wenzelm
# Date 1674216718 -3600
# Node ID 474a07221c276afea160844059de41aaaf11574e
# Parent  ac5ebdf198613b6b8e82310932e23cd231964bad
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;

diff -r ac5ebdf19861 -r 474a07221c27 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jan 20 13:08:54 2023 +0100
+++ b/src/Pure/Thy/export.scala	Fri Jan 20 13:11:58 2023 +0100
@@ -434,6 +434,29 @@
     def source_file(name: String): Sessions.Source_File =
       get_source_file(name).getOrElse(error("Missing session source file " + quote(name)))
 
+    def theory_source(theory: String, unicode_symbols: Boolean = false): String = {
+      def snapshot_source: Option[String] =
+        for {
+          snapshot <- document_snapshot
+          text <- snapshot.version.nodes.iterator.collectFirst(
+            { case (name, node) if name.theory == theory => node.source })
+          if text.nonEmpty
+        } yield Symbol.output(unicode_symbols, text)
+
+      def db_source: Option[String] = {
+        val theory_context = session_context.theory(theory)
+        for {
+          name <- theory_context.files0(permissive = true).headOption
+          file <- get_source_file(name)
+        } yield {
+          val text0 = file.bytes.text
+          if (unicode_symbols) Symbol.decode(text0) else text0
+        }
+      }
+
+      snapshot_source orElse db_source getOrElse ""
+    }
+
     def classpath(): List[File.Content] = {
       (for {
         session <- session_stack.iterator