Allow Agda to output data files

[wenkokke]

The current method for obtaining agda.sty and agda.css which are consistent with the Agda version you're using is to compile some Agda code, and wait for Agda to fill it in. It may be a good idea to add a --dump-data-file command, which, when passed a filename, outputs the corresponding data file to stdout.

[andreasabel]

Isn't --print-agda-dir good enough already? (#5005)

$ cat $(agda --print-agda-dir)/latex/agda.sty
...
$ cat $(agda --print-agda-dir)/html/Agda.css
...

So maybe it is more like a documentation issue?

[wenkokke]

Oh, thanks, didn't realise this!