# HG changeset patch
# User wenzelm
# Date 1663869897 -7200
# Node ID 005abcb34849fb9779b7a609b8d6b2036b8950e8
# Parent  b80b2fbc46c3de170adaf6221808638a0e45a170
tuned signature;

diff -r b80b2fbc46c3 -r 005abcb34849 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Thu Sep 22 17:24:50 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Thu Sep 22 20:04:57 2022 +0200
@@ -599,11 +599,10 @@
       def err(): Nothing =
         error("Missing document information for theory: " + quote(theory_name))
 
-      val command = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err()
+      val snapshot = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err()
       val theory = context.theory_by_name(session_name, theory_name) getOrElse err()
 
       if (verbose) progress.echo("Presenting theory " + quote(theory_name))
-      val snapshot = Document.State.init.snippet(command)
 
       val thy_elements = theory.elements(context.elements)
 
diff -r b80b2fbc46c3 -r 005abcb34849 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Sep 22 17:24:50 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Thu Sep 22 20:04:57 2022 +0200
@@ -17,7 +17,7 @@
   def read_theory(
     theory_context: Export.Theory_Context,
     unicode_symbols: Boolean = false
-  ): Option[Command] = {
+  ): Option[Document.Snapshot] = {
     def read(name: String): Export.Entry = theory_context(name, permissive = true)
 
     def read_xml(name: String): XML.Body =
@@ -74,8 +74,11 @@
           for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
           yield index -> Markup_Tree.from_XML(xml))
 
-      Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
-        blobs_info = blobs_info, results = results, markups = markups)
+      val command =
+        Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
+          blobs_info = blobs_info, results = results, markups = markups)
+
+      Document.State.init.snippet(command)
     }
   }
 
@@ -128,18 +131,17 @@
 
               read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
                 case None => progress.echo(thy_heading + " MISSING")
-                case Some(command) =>
-                  val snapshot = Document.State.init.snippet(command)
+                case Some(snapshot) =>
                   val rendering = new Rendering(snapshot, options, session)
                   val messages =
                     rendering.text_messages(Text.Range.full)
                       .filter(message => verbose || Protocol.is_exported(message.info))
                   if (messages.nonEmpty) {
-                    val line_document = Line.Document(command.source)
+                    val line_document = Line.Document(snapshot.source)
                     val buffer = new mutable.ListBuffer[String]
                     for (Text.Info(range, elem) <- messages) {
                       val line = line_document.position(range.start).line1
-                      val pos = Position.Line_File(line, command.node_name.node)
+                      val pos = Position.Line_File(line, snapshot.node_name.node)
                       def message_text: String =
                         Protocol.message_text(elem, heading = true, pos = pos,
                           margin = margin, breakgain = breakgain, metric = metric)
diff -r b80b2fbc46c3 -r 005abcb34849 src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Thu Sep 22 17:24:50 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Thu Sep 22 20:04:57 2022 +0200
@@ -29,8 +29,7 @@
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              command <- Build_Job.read_theory(session_context.theory(thy)).iterator
-              snapshot = Document.State.init.snippet(command)
+              snapshot <- Build_Job.read_theory(session_context.theory(thy)).iterator
               (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList