# HG changeset patch
# User wenzelm
# Date 1674141761 -3600
# Node ID 5292286908a47a98c4a1b9399af3bc8810db3fe5
# Parent  05219e08c3e9702daf5451e8173aa5c6522449ff
clarified "selected" status;

diff -r 05219e08c3e9 -r 5292286908a4 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Thu Jan 19 16:17:24 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Thu Jan 19 16:22:41 2023 +0100
@@ -233,8 +233,10 @@
     lazy val document_latex: List[Document_Latex] =
       for (name <- all_document_theories)
       yield {
+        val selected = document_selection(name)
+
         val body =
-          if (document_selection(name)) {
+          if (selected) {
             val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
             YXML.parse_body(entry.text)
           }
@@ -242,12 +244,15 @@
 
         def line_pos(props: Properties.T): Option[Int] =
           Position.Line.unapply(props) orElse {
-            for {
-              snapshot <- session_context.document_snapshot
-              id <- Position.Id.unapply(props)
-              offset <- Position.Offset.unapply(props)
-              line <- snapshot.find_command_line(id, offset)
-            } yield line
+            if (selected) {
+              for {
+                snapshot <- session_context.document_snapshot
+                id <- Position.Id.unapply(props)
+                offset <- Position.Offset.unapply(props)
+                line <- snapshot.find_command_line(id, offset)
+              } yield line
+            }
+            else None
           }
 
         Document_Latex(name, body, line_pos)