proper line positions for PIDE document;

--- a/src/Pure/Thy/document_build.scala	Wed Jan 18 11:32:27 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Jan 18 14:18:31 2023 +0100
@@ -141,11 +141,16 @@
       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(
@@ -234,7 +239,18 @@
             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)
       }
 
 

--- a/src/Pure/Thy/export.scala	Wed Jan 18 11:32:27 2023 +0100
+++ b/src/Pure/Thy/export.scala	Wed Jan 18 14:18:31 2023 +0100
@@ -346,7 +346,7 @@
     val database_context: Database_Context,
     session_background: Sessions.Background,
     db_hierarchy: List[Session_Database],
-    document_snapshot: Option[Document.Snapshot]
+    val document_snapshot: Option[Document.Snapshot]
   ) extends AutoCloseable {
     session_context =>
 

--- a/src/Pure/Thy/latex.scala	Wed Jan 18 11:32:27 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Jan 18 14:18:31 2023 +0100
@@ -261,7 +261,11 @@
       error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
         ":\n" + XML.string_of_tree(elem))
 
-    def make(latex_text: Text, file_pos: String = ""): String = {
+    def make(
+      latex_text: Text,
+      file_pos: String = "",
+      line_pos: Properties.T => Option[Int] = Position.Line.unapply
+    ): String = {
       var line = 1
       val result = new mutable.ListBuffer[String]
       val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
@@ -278,9 +282,11 @@
             traverse {
               markup match {
                 case Markup.Document_Latex(props) =>
-                  for (l <- Position.Line.unapply(props) if positions.nonEmpty) {
-                    val s = position(Value.Int(line), Value.Int(l))
-                    if (positions.last != s) positions += s
+                  if (positions.nonEmpty) {
+                    for (l <- line_pos(props)) {
+                      val s = position(Value.Int(line), Value.Int(l))
+                      if (positions.last != s) positions += s
+                    }
                   }
                   body
                 case Markup.Latex_Output(_) => XML.string(latex_output(body))