williamdemeo
commented
1 year ago I wrote such a script (in Scala) and it does okay, but the output needs quite a bit of hand-tweaking. For example, the script cannot choose a good name for the macro when the token involves unicode symbols.
Here's a more complicated example than those mentioned above in the issue description:
If we want _⊢_⇀⦇_,RATIFY⦈_ to appear in the documentation, we could use the following latex macro to typeset it:
\newcommand{\RATIFYtransition}{\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀⦇\AgdaUnderscore{},RATIFY⦈\AgdaUnderscore{}}}\xspace}
The script I wrote can construct almost all of this macro by extracting the Agda formatting from the Ratify.tex file that Agda generates from the Ratify.lagda file. The only part it can't create is the name \RATIFYtransition that I chose... and since I can't even decide if that's a reasonable name, I certainly can't expect the script to do so 😆
But if all we have to do is select names for the macros produced by the script, that should relieve us of a non-trivial amount of tedious typesetting.
WhatisRT
In recent work I spent more time trying to properly typeset Agda tokens that appear in documentation than on making sure the prose is correct and well-written.
To address this, I suggest we develop a script that reads in the tex produced by agda (from our .lagda files) and extracts all tokens along with the appropriate tex macros for formatting them and places these in a macro file. With such a utility, we can simply use, e.g., \GovAction instead of \AgdaRecord{GovAction} in the documentation.
It might seem this merely saves a few key strokes but the problem when documenting a large Agda module (especially when you're not the original author of the module) is that it can be tedious and distracting to try to remember or look up whether we want, e.g., \AgdaRecord{GovAction} instead of \AgdaDatatype{GovAction}.