Discussion:
[isabelle] \<^descr>
(too old to reply)
Peter Lammich
2016-08-02 09:45:32 UTC
Permalink
Raw Message
Hi all,

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?

--
Peter
Makarius
2016-08-02 09:55:24 UTC
Permalink
Raw Message
Post by Peter Lammich
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
Peter Lammich
2016-08-02 10:34:34 UTC
Permalink
Raw Message
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.

--
Peter
Post by Makarius
Post by Peter Lammich
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
Makarius
2016-08-02 13:29:20 UTC
Permalink
Raw Message
Post by Peter Lammich
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.
There is no need to invent a different syntax for Isabelle. It can parse
the [...] notation as in LaTeX.


Makarius

Loading...