src/Pure/Thy/document_build.scala

     for {
       s1 <- Library.try_unprefix("Running program \"", s)
       s2 <- Library.try_unsuffix("\" ...", s1)
     } yield s2
 
-  sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
+  sealed case class Document_Latex(
+    name: Document.Node.Name,
+    body: XML.Body,
+    line_pos: Properties.T => Option[Int]
+  ) {
     def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
     def file_pos: String = File.symbolic_path(name.path)
     def write(latex_output: Latex.Output, dir: Path): Unit =
-      content.output(latex_output.make(_, file_pos = file_pos)).write(dir)
+      content.output(latex_output.make(_, file_pos = file_pos, line_pos = line_pos))
+        .write(dir)
   }
 
   def context(
     session_context: Export.Session_Context,
     document_session: Option[Sessions.Base] = None,

           if (document_selection(name)) {
             val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
             YXML.parse_body(entry.text)
           }
           else Nil
-        Document_Latex(name, body)
+
+        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)
+              pos <- snapshot.find_command_position(id, offset)
+            } yield pos.line1
+          }
+
+        Document_Latex(name, body, line_pos)
       }
 
 
     /* build document */