Email Gateway (Aug 22 2022 at 20:46): Email Gateway (Aug 22 2022 at 20:46):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
The Isabelle/Isar Reference Manual says that \<^descr> can be used to
mark up description list items. However, a description list item
contains two parts: a term and a description. How do you specify what
the term and what the description is?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:46):From: Makarius <makarius@sketis.net>
You merely let LaTeX do it: \<^descr>[abc] blah
You can see this in the existing documents, e.g. $ISABELLE_HOME/src/Doc/.
Makarius
Email Gateway (Aug 22 2022 at 20:46):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hmm, it seems a bit inconsistent that the markup that tells it’s a
description item is part of Isabelle but the markup that distinguishes
the term from the description is not. Are there any plans to introduce
Isabelle markup for the latter as well?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:46):From: Makarius <makarius@sketis.net>
Isabelle/PIDE markup is always an approximation, and gradually becomes
more complete over the years.
For \<^descr> the plan is to have the Isabelle Markdown parser accept
the LaTeX syntax and report its structure properly.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC