At 2018-04-21T17:29:58+02:00, Wolfgang Schuster wrote:
> The verbatim commands have a range key which let you select parts of
> the code, you can use line numbers to include a small block
> (e.g. range={3,10} or range {3,+7}) or you put labels in your code.
Many thanks! It works perfectly, with something like this:
\starttext
\typefile
[range={beg:8e1e0cb9:6524:4a9b:a58e:6610c8bcf156,
end:8e1e0cb9:6524:4a9b:a58e:6610c8bcf156}]
{../coq/univalence/transport/total_path.v}
\typefile
[range={beg:8edf79a4:6fe4:4a0c:a1a4:5be2ab413b47,
end:8edf79a4:6fe4:4a0c:a1a4:5be2ab413b47}]
{../coq/univalence/transport/path_from.v}
\stoptext
Raghu.
--
N. Raghavendra <ra...@hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/
___________________________________________________________________________________
If your question is of interest to others as well, please add an entry to the
Wiki!
maillist : ntg-context@ntg.nl / http://www.ntg.nl/mailman/listinfo/ntg-context
webpage : http://www.pragma-ade.nl / http://context.aanhet.net
archive : https://bitbucket.org/phg/context-mirror/commits/
wiki : http://contextgarden.net
___________________________________________________________________________________
