[NTG-context] Including part of a program source file

N. Raghavendra nyraghu27132 at gmail.com
Sat Apr 21 20:51:25 CEST 2018


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 <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/


More information about the ntg-context mailing list