--- 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 *)