# HG changeset patch # User wenzelm # Date 1673549327 -3600 # Node ID e47fb5cfef411f0b534d28c4cc57802f26108d1c # Parent 3f25c28c42570db49a031cb1086e93eb180d4497 clarified Latex markup: optional cite "location" consists of nested document text; diff -r 3f25c28c4257 -r e47fb5cfef41 src/Pure/PIDE/markup.ML --- 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; diff -r 3f25c28c4257 -r e47fb5cfef41 src/Pure/PIDE/markup.scala --- 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) diff -r 3f25c28c4257 -r e47fb5cfef41 src/Pure/Thy/bibtex.ML --- 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>\cite_macro\ (Config.put cite_macro) #> Document_Output.antiquotation_raw \<^binding>\cite\ - (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; diff -r 3f25c28c4257 -r e47fb5cfef41 src/Pure/Thy/latex.ML --- 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 *) diff -r 3f25c28c4257 -r e47fb5cfef41 src/Pure/Thy/latex.scala --- 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(_) =>