# HG changeset patch
# User wenzelm
# Date 1637596198 -3600
# Node ID f31229171b3bc66a751cb0c77e3b69567f426d72
# Parent  46c7fafbea3d3efb0bc42938a26ac34ca8a8355e
source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;

diff -r 46c7fafbea3d -r f31229171b3b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Nov 22 15:03:37 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Nov 22 16:49:58 2021 +0100
@@ -778,6 +778,8 @@
 {
   def is_empty: Boolean = name.isEmpty
 
+  def position_properties: Position.T = properties.filter(Markup.position_property)
+
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
diff -r 46c7fafbea3d -r f31229171b3b src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Mon Nov 22 15:03:37 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Mon Nov 22 16:49:58 2021 +0100
@@ -184,8 +184,8 @@
 datatype token =
     Ignore
   | Token of Token.T
-  | Heading of string * Input.source
-  | Body of string * Input.source
+  | Heading of Markup.T * Input.source
+  | Body of Markup.T * Input.source
   | Raw of Input.source;
 
 fun token_with pred (Token tok) = pred tok
@@ -200,13 +200,17 @@
   (case tok of
     Ignore => []
   | Token tok => output_token ctxt tok
-  | Heading (kind, source) =>
-      [XML.Elem (Markup.latex_heading kind, output_document ctxt {markdown = false} source)]
-  | Body (kind, source) =>
-      [XML.Elem (Markup.latex_body kind, output_document ctxt {markdown = true} source)]
+  | Heading (markup, source) => [XML.Elem (markup, output_document ctxt {markdown = false} source)]
+  | Body (markup, source) => [XML.Elem (markup, output_document ctxt {markdown = true} source)]
   | Raw source =>
       Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n");
 
+fun mk_heading (kind, pos) source =
+  Heading (Markup.latex_heading kind |> Position.markup pos, source);
+
+fun mk_body (kind, pos) source =
+  Body (Markup.latex_body kind |> Position.markup pos, source);
+
 
 (* command spans *)
 
@@ -384,14 +388,15 @@
 
     fun markup pred mk flag = Scan.peek (fn d =>
       Document_Source.improper |--
-        Parse.position (Scan.one (fn tok =>
-          Token.is_command tok andalso pred keywords (Token.content_of tok))) --
+        Scan.one (fn tok => Token.is_command tok andalso pred keywords (Token.content_of tok)) --
       (Document_Source.annotation |--
         Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
           Parse.document_source --| Document_Source.improper_end))
-            >> (fn ((tok, pos'), source) =>
-              let val name = Token.content_of tok
-              in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
+            >> (fn (tok, source) =>
+              let
+                val kind = Token.content_of tok;
+                val pos' = Token.pos_of tok;
+              in (SOME (kind, pos'), (mk (kind, pos') source, (flag, d))) end));
 
     val command = Scan.peek (fn d =>
       Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
@@ -409,9 +414,9 @@
 
     val tokens =
       (ignored ||
-        markup Keyword.is_document_heading Heading markup_true ||
-        markup Keyword.is_document_body Body markup_true ||
-        markup Keyword.is_document_raw (Raw o #2) "") >> single ||
+        markup Keyword.is_document_heading mk_heading markup_true ||
+        markup Keyword.is_document_body mk_body markup_true ||
+        markup Keyword.is_document_raw (K Raw) "") >> single ||
       command ||
       (cmt || other) >> single;
 
diff -r 46c7fafbea3d -r f31229171b3b src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Mon Nov 22 15:03:37 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Nov 22 16:49:58 2021 +0100
@@ -116,10 +116,10 @@
     def latex_environment(name: String, body: Text): Text =
       XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body)
 
-    def latex_heading(kind: String, body: Text): Text =
+    def latex_heading(kind: String, pos: Position.T, body: Text): Text =
       XML.enclose("%\n\\" + options.string("document_heading_prefix") + kind + "{", "%\n}\n", body)
 
-    def latex_body(kind: String, body: Text): Text =
+    def latex_body(kind: String, pos: Position.T, body: Text): Text =
       latex_environment("isamarkup" + kind, body)
 
     def latex_delim(name: String, body: Text): Text =
@@ -177,10 +177,10 @@
             traverse(latex_macro(name, body))
           case XML.Elem(Markup.Latex_Environment(name), body) =>
             traverse(latex_environment(name, body))
-          case XML.Elem(Markup.Latex_Heading(kind), body) =>
-            traverse(latex_heading(kind, body))
-          case XML.Elem(Markup.Latex_Body(kind), body) =>
-            traverse(latex_body(kind, body))
+          case XML.Elem(markup @ Markup.Latex_Heading(kind), body) =>
+            traverse(latex_heading(kind, markup.position_properties, body))
+          case XML.Elem(markup @ Markup.Latex_Body(kind), body) =>
+            traverse(latex_body(kind, markup.position_properties, body))
           case XML.Elem(Markup.Latex_Delim(name), body) =>
             traverse(latex_delim(name, body))
           case XML.Elem(Markup.Latex_Tag(name), body) =>