NEWS: more LaTeX markup

[Makarius]

On 11/12/2024 17:25, Tobias Nipkow wrote:
> 
> Is there any way to obtain (in the document} \isaconst{Nil} via some 
> antiquotation?
> - @{const Nil} produces []
> - @{const [source] Nil} produces \isa{Nil}
> 
> Of course this is just an example standing for the many constants that have 
> associated syntax.

@{const [source] NAME} presents the original input source, not pretty-printed 
output. It would require substantial reworking of the document preparation 
system to use PIDE markup there: one happy day that will happen, but not now 
and not for the coming release.

If this is actually about printing formal entity names like the term 
pretty-printer does (without syntax), you can define a document antiquotation 
@{const_name NAME} like this:

setup ‹
   Document_Output.antiquotation_pretty_embedded \<^binding>‹const_name›
     (Args.const {proper = true, strict = false})
     (fn ctxt => fn c => Pretty.mark_str (Markup.const, 
Proof_Context.extern_const ctxt c))
›


	Makarius