Re: [isabelle] How to mark up terms and descriptions?

On 19/10/2019 14:38, Wolfgang Jeltsch wrote:
> Am Samstag, den 19.10.2019, 13:35 +0200 schrieb Makarius:
>> On 18/10/2019 23:58, Wolfgang Jeltsch wrote:
>> 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?
>> You merely let LaTeX do it: \<^descr>[abc] blah
>> You can see this in the existing documents, e.g. $ISABELLE_HOME/src/Doc/.
> 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?

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.