diff -r dab089b25eb6 -r 865b44cbaad1 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Jul 09 17:39:46 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Sun Jul 09 17:41:02 2023 +0200
@@ -527,74 +527,4 @@
     override def is_finished: Boolean = future_result.is_finished
     override def join: (Process_Result, SHA1.Shasum) = future_result.join
   }
-
-
-  /* theory markup/messages from session database */
-
-  def read_theory(
-    theory_context: Export.Theory_Context,
-    unicode_symbols: Boolean = false
-  ): Option[Document.Snapshot] = {
-    def decode_bytes(bytes: Bytes): String =
-      Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes))
-
-    def read(name: String): Export.Entry = theory_context(name, permissive = true)
-
-    def read_xml(name: String): XML.Body =
-      YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache)
-
-    def read_source_file(name: String): Store.Source_File =
-      theory_context.session_context.source_file(name)
-
-    for {
-      id <- theory_context.document_id()
-      (thy_file, blobs_files) <- theory_context.files(permissive = true)
-    }
-    yield {
-      val master_dir =
-        Path.explode(Url.strip_base_name(thy_file).getOrElse(
-          error("Cannot determine theory master directory: " + quote(thy_file))))
-
-      val blobs =
-        blobs_files.map { name =>
-          val path = Path.explode(name)
-          val src_path = File.relative_path(master_dir, path).getOrElse(path)
-
-          val file = read_source_file(name)
-          val bytes = file.bytes
-          val text = decode_bytes(bytes)
-          val chunk = Symbol.Text_Chunk(text)
-
-          Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) ->
-            Document.Blobs.Item(bytes, text, chunk, changed = false)
-        }
-
-      val thy_source = decode_bytes(read_source_file(thy_file).bytes)
-      val thy_xml = read_xml(Export.MARKUP)
-      val blobs_xml =
-        for (i <- (1 to blobs.length).toList)
-          yield read_xml(Export.MARKUP + i)
-
-      val markups_index = Command.Markup_Index.make(blobs.map(_._1))
-      val markups =
-        Command.Markups.make(
-          for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
-          yield index -> Markup_Tree.from_XML(xml))
-
-      val results =
-        Command.Results.make(
-          for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
-            yield i -> elem)
-
-      val command =
-        Command.unparsed(thy_source, theory = true, id = id,
-          node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
-          blobs_info = Command.Blobs_Info.make(blobs),
-          markups = markups, results = results)
-
-      val doc_blobs = Document.Blobs.make(blobs)
-
-      Document.State.init.snippet(command, doc_blobs)
-    }
-  }
 }