Re: [isabelle] \<^descr>

So the structure of this high-level structuring mechanism is only
established at low-level latex, that happens to interpret the [name]
(which is just plain text for Isabelle) as optional argument to the
\item generated by \<^descr>. 

Regarding the (long-time) goal to output to different formats than latex
(eg html), I would have expected the (name,text) structure of
description items to be already established on Isabelle-level.


On Di, 2016-08-02 at 11:52 +0200, Makarius wrote:
> On 02/08/16 11:42, Peter Lammich wrote:
> > 
> > according to the isar-ref manual, \<^descr> shall be a markdown-like
> > version for description. However, it is nowhere documented how to
> > specify the name for the item. Also a quick inspection of the source
> > code gives no clues.
> > 
> > Any hints?
> \<^descr>[name]
> See also the sources as examples, e.g. src/Doc/Isar_Ref.
> 	Makarius

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