(Re)Documenting catchfilebetweentags method of building latex files with Agda

[JacquesCarette]

There are two methods to do this, the one that used to be documented using catchfilebetweentags, and one using \newcommand.

The documentation only mentions the latter now, while it used to only mention the earlier. This change was done by @nad in 38c0322 but there is no rationale given for why one method is preferred.

I suggest that both options be documented, and users left to choose. [If this is agreeable, I can do it.]

[nad]

I don't see a problem with including both methods, if they have different use cases. Is the point of the method that uses catchfilebetweentags that the Agda code does not need to be in a LaTeX file? The currently documented method can be used inside a single .lagda.tex file if you want to present code in an order that does not match the order imposed by Agda.