Anyweb, Document Source Code The Way You Like
I was playing with Adam Chlipala's “CPDT” book and I wanted to take notes on some notations. I also wanted to do it in a Literate Programming way: in a .v Coq file with a familiar and practical syntax …
That's where Anyweb comes into play.
This one-day hack is a simple parser and printer which looks for special string-markers (like (*B and B*) in Coq or OCaml sources) and does stuff (like calling coqdoc or source-highlight) depending on where it is in the source. The transformer uses an automaton and a stack, so any kind of recursive embedding seems possible.
