I recently discovered this great program that includes support for literate programming. Very nicely done! Although focused on SML and proofs, it has ability to be extended to other languages:

Rob, I am really enjoying learning about ProofPower and so impressed at the amount of documentation and extra facilities that I didn't even know were part of this program. e.g. I have long been interested in "literate programming" and find your approach using =SML and =TEX to be very efficient. I read in the usr001.pdf that it is possible to add other languages such as =C but don't quite see what I have to do to make that work. I tried just putting =C followed by the some C code, but got errors from docsml that say =C is not defined.
The example is from page 56 in the section about sieve so I imagine the info is there somewhere, but I find that section a bit difficult for me at this early stage of learning about ProofPower. I found I can use =DUMP to get a similar effect, however in the document =C would certainly be more descriptive.
-Dave
p.s. I am cc'ing the literate programming group to this discussion because I think there may be others that do not know about ProofPower and its support for literate programming.