clarified modules (amending 570f65953173);

--- a/src/Pure/Thy/browser_info.scala	Sun Jul 09 17:39:46 2023 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Jul 09 17:41:02 2023 +0200
@@ -598,7 +598,7 @@
       def err(): Nothing =
         error("Missing document information for theory: " + quote(theory_name))
 
-      val snapshot = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err()
+      val snapshot = Build.read_theory(session_context.theory(theory_name)) getOrElse err()
       val theory = context.theory_by_name(session_name, theory_name) getOrElse err()
 
       progress.echo("Presenting theory " + quote(theory_name), verbose = true)

--- a/src/Pure/Tools/build.scala	Sun Jul 09 17:39:46 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Jul 09 17:41:02 2023 +0200
@@ -643,7 +643,7 @@
             for (thy <- print_theories) {
               val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":"
 
-              Build_Job.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
+              Build.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
                 case None => progress.echo(thy_heading + " MISSING")
                 case Some(snapshot) =>
                   val rendering = new Rendering(snapshot, options, session)

--- 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)
-    }
-  }
 }

--- a/src/Pure/Tools/profiling_report.scala	Sun Jul 09 17:39:46 2023 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Sun Jul 09 17:41:02 2023 +0200
@@ -29,7 +29,7 @@
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              snapshot <- Build_Job.read_theory(session_context.theory(thy)).iterator
+              snapshot <- Build.read_theory(session_context.theory(thy)).iterator
               (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList
 

--- a/src/Pure/Tools/update.scala	Sun Jul 09 17:39:46 2023 +0200
+++ b/src/Pure/Tools/update.scala	Sun Jul 09 17:41:02 2023 +0200
@@ -109,7 +109,7 @@
             seen_theory += theory
             val theory_context = session_context.theory(theory)
             for {
-              theory_snapshot <- Build_Job.read_theory(theory_context)
+              theory_snapshot <- Build.read_theory(theory_context)
               node_name <- theory_snapshot.node_files
               snapshot = theory_snapshot.switch(node_name)
               if snapshot.node.source_wellformed