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