clarified Latex markup: optional cite "location" consists of nested document text;

--- a/src/Pure/PIDE/markup.ML	Thu Jan 12 16:01:49 2023 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 12 19:48:47 2023 +0100
@@ -155,7 +155,7 @@
   val latex_environmentN: string val latex_environment: string -> T
   val latex_headingN: string val latex_heading: string -> T
   val latex_bodyN: string val latex_body: string -> T
-  val latex_citeN: string val latex_cite: {kind: string, location: string} -> T
+  val latex_citeN: string val latex_cite: {kind: string, citation: string} -> T
   val latex_index_itemN: string val latex_index_item: T
   val latex_index_entryN: string val latex_index_entry: string -> T
   val latex_delimN: string val latex_delim: string -> T
@@ -592,10 +592,10 @@
 val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN;
 val (latex_bodyN, latex_body) = markup_string "latex_body" kindN;
 val (latex_citeN, _) = markup_elem "latex_cite";
-fun latex_cite {kind, location} =
+fun latex_cite {kind, citation} =
   (latex_citeN,
     (if kind = "" then [] else [(kindN, kind)]) @
-    (if location = "" then [] else [("cite_location", location)]));
+    (if citation = "" then [] else [("citation", citation)]));
 val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item";
 val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN;
 val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN;

--- a/src/Pure/PIDE/markup.scala	Thu Jan 12 16:01:49 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 12 19:48:47 2023 +0100
@@ -363,7 +363,7 @@
   val Latex_Tag = new Markup_String("latex_tag", NAME)
 
   val Latex_Cite = new Markup_Elem("latex_cite")
-  val Cite_Location = new Properties.String("cite_location")
+  val Citation_ = new Properties.String("citation")
 
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)

--- a/src/Pure/Thy/bibtex.ML	Thu Jan 12 16:01:49 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Thu Jan 12 19:48:47 2023 +0100
@@ -42,12 +42,14 @@
   Theory.setup
    (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
     Document_Output.antiquotation_raw \<^binding>\<open>cite\<close>
-      (Scan.lift (Scan.optional Parse.cartouche "" -- Parse.and_list1 Args.name_position))
-      (fn ctxt => fn (location, citations) =>
+      (Scan.lift (Scan.option Args.cartouche_input -- Parse.and_list1 Args.name_position))
+      (fn ctxt => fn (opt_loc, citations) =>
         let
+          val loc = the_default Input.empty opt_loc;
           val _ =
             Context_Position.reports ctxt
-              (map (fn (name, pos) => (pos, Markup.citation name)) citations);
+              (Document_Output.document_reports loc @
+                map (fn (name, pos) => (pos, Markup.citation name)) citations);
 
           val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
           val bibtex_entries = Resources.theory_bibtex_entries thy_name;
@@ -59,6 +61,7 @@
                 else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
           val kind = Config.get ctxt cite_macro;
-        in Latex.cite {kind = kind, location = location, citations = citations} end));
+          val location = Document_Output.output_document ctxt {markdown = false} loc;
+        in Latex.cite {kind = kind, citations = citations, location = location} end));
 
 end;

--- a/src/Pure/Thy/latex.ML	Thu Jan 12 16:01:49 2023 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Jan 12 19:48:47 2023 +0100
@@ -23,7 +23,7 @@
   val symbols_output: Symbol_Pos.T list -> text
   val isabelle_body: string -> text -> text
   val theory_entry: string -> string
-  val cite: {kind: string, location: string, citations: (string * Position.T) list} -> text
+  val cite: {kind: string, citations: (string * Position.T) list, location: text} -> text
   type index_item = {text: text, like: string}
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
@@ -201,14 +201,14 @@
 
 fun cite {kind, location, citations} =
   let
-    val markup = Markup.latex_cite {kind = kind, location = location};
     val _ =
       citations |> List.app (fn (s, pos) =>
         if exists_string (fn c => c = ",") s
         then error ("Single citation expected, without commas" ^ Position.here pos)
         else ());
-    val args = space_implode "," (map #1 citations);
-  in [XML.Elem (markup, XML.string args)] end;
+    val citation = space_implode "," (map #1 citations);
+    val markup = Markup.latex_cite {kind = kind, citation = citation};
+  in [XML.Elem (markup, location)] end;
 
 
 (* index entries *)

--- a/src/Pure/Thy/latex.scala	Thu Jan 12 16:01:49 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Jan 12 19:48:47 2023 +0100
@@ -49,14 +49,13 @@
   /* cite: references to bibliography */
 
   object Cite {
-    sealed case class Value(kind: String, location: String, citations: String)
+    sealed case class Value(kind: String, citation: String, location: XML.Body)
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
           val kind = Markup.Kind.unapply(props).getOrElse("cite")
-          val location = Markup.Cite_Location.unapply(props).getOrElse("")
-          val citations = XML.content(body)
-          Some(Value(kind, location, citations))
+          val citation = Markup.Citation_.unapply(props).getOrElse("")
+          Some(Value(kind, citation, body))
         case _ => None
       }
   }
@@ -211,6 +210,13 @@
       }
     }
 
+    def cite(value: Cite.Value): Text = {
+      latex_macro0(value.kind) :::
+      (if (value.location.isEmpty) Nil
+       else XML.string("[") ::: value.location ::: XML.string("]")) :::
+      XML.string("{" + value.citation + "}")
+    }
+
     def index_item(item: Index_Item.Value): String = {
       val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
       val text = index_escape(latex_output(item.text))
@@ -262,9 +268,7 @@
                 case Markup.Latex_Tag(name) => latex_tag(name, body)
                 case Markup.Latex_Cite(_) =>
                   elem match {
-                    case Cite(cite) =>
-                      val opt = if (cite.location.isEmpty) "" else "[" + cite.location + "]"
-                      latex_macro(cite.kind, XML.string(cite.citations), optional_argument = opt)
+                    case Cite(value) => cite(value)
                     case _ => unknown_elem(elem, file_position)
                   }
                 case Markup.Latex_Index_Entry(_) =>