more explicit latex markup;

--- a/src/Pure/PIDE/markup.ML	Wed Jan 11 15:00:06 2023 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 12 16:01:49 2023 +0100
@@ -155,6 +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_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
@@ -590,6 +591,11 @@
 val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN;
 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} =
+  (latex_citeN,
+    (if kind = "" then [] else [(kindN, kind)]) @
+    (if location = "" then [] else [("cite_location", location)]));
 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	Wed Jan 11 15:00:06 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 12 16:01:49 2023 +0100
@@ -362,6 +362,9 @@
   val Latex_Delim = new Markup_String("latex_delim", NAME)
   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 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	Wed Jan 11 15:00:06 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Thu Jan 12 16:01:49 2023 +0100
@@ -42,8 +42,8 @@
   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.option Parse.cartouche -- Parse.and_list1 Args.name_position))
-      (fn ctxt => fn (opt, citations) =>
+      (Scan.lift (Scan.optional Parse.cartouche "" -- Parse.and_list1 Args.name_position))
+      (fn ctxt => fn (location, citations) =>
         let
           val _ =
             Context_Position.reports ctxt
@@ -58,8 +58,7 @@
                 if member (op =) bibtex_entries name then ()
                 else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
-          val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
-          val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
-        in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
+          val kind = Config.get ctxt cite_macro;
+        in Latex.cite {kind = kind, location = location, citations = citations} end));
 
 end;

--- a/src/Pure/Thy/latex.ML	Wed Jan 11 15:00:06 2023 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Jan 12 16:01:49 2023 +0100
@@ -23,6 +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
   type index_item = {text: text, like: string}
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
@@ -196,6 +197,20 @@
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
 
 
+(* cite: references to bibliography *)
+
+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;
+
+
 (* index entries *)
 
 type index_item = {text: text, like: string};

--- a/src/Pure/Thy/latex.scala	Wed Jan 11 15:00:06 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Thu Jan 12 16:01:49 2023 +0100
@@ -46,6 +46,22 @@
     else name
 
 
+  /* cite: references to bibliography */
+
+  object Cite {
+    sealed case class Value(kind: String, location: String, citations: String)
+    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))
+        case _ => None
+      }
+  }
+
+
   /* index entries */
 
   def index_escape(str: String): String = {
@@ -244,6 +260,13 @@
                 case Markup.Latex_Body(kind) => latex_body(kind, body, a)
                 case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true)
                 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 _ => unknown_elem(elem, file_position)
+                  }
                 case Markup.Latex_Index_Entry(_) =>
                   elem match {
                     case Index_Entry(entry) => index_entry(entry)