Export, Edition, PDF format

Add a new export command to produce one PDF per Text edition.

See existing Java tools that can:

- convert HTML to PDF using the CSS styling

• merge PDFs (or create one PDF with several HTMLs - or create one PDF from a TXM edition made of a single HTML page)

See:

• Native Java library
  • Open HTML to PDF: https://github.com/danfickle/openhtmltopdf (flying-saucer + pdfbox)
• Pandoc external call (to generate several formats: pdf, odt, docx…)
  • PandaDoc SDK: https://github.com/PandaDoc/pandadoc-api-java-client

(from redmine: issue id 3561, created on 2023/12/22 by Matthieu Decorde)