diff -r 52f3d1cd8d63 -r 3f25c28c4257 src/Pure/PIDE/markup.ML --- 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;