# HG changeset patch # User wenzelm # Date 1673535709 -3600 # Node ID 3f25c28c42570db49a031cb1086e93eb180d4497 # Parent 52f3d1cd8d638774570660bd04d438ca42366bf7 more explicit latex markup; 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; diff -r 52f3d1cd8d63 -r 3f25c28c4257 src/Pure/PIDE/markup.scala --- 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) diff -r 52f3d1cd8d63 -r 3f25c28c4257 src/Pure/Thy/bibtex.ML --- 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>\cite_macro\ (Config.put cite_macro) #> Document_Output.antiquotation_raw \<^binding>\cite\ - (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; diff -r 52f3d1cd8d63 -r 3f25c28c4257 src/Pure/Thy/latex.ML --- 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}; diff -r 52f3d1cd8d63 -r 3f25c28c4257 src/Pure/Thy/latex.scala --- 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)