# HG changeset patch
# User wenzelm
# Date 1673020243 -3600
# Node ID fffb978dd683a25516aff8db1a74b4059d0b3bcf
# Parent  dd53bb198eb1e89950dd89eae4db9b588cbe3924
removed unused operation: unclear wrt. Symbol.encode/decode status;

diff -r dd53bb198eb1 -r fffb978dd683 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jan 06 16:43:51 2023 +0100
+++ b/src/Pure/Thy/export.scala	Fri Jan 06 16:50:43 2023 +0100
@@ -434,23 +434,6 @@
     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 {
-          snapshot <- document_snapshot
-          node = snapshot.get_node(name)
-          text = node.source if text.nonEmpty
-        } yield text
-
-      def db_source: String =
-        get_source_file(name.node) match {
-          case Some(file) => file.text
-          case None => ""
-        }
-
-      snapshot_source getOrElse db_source
-    }
-
     def classpath(): List[File.Content] = {
       (for {
         session <- session_stack.iterator