JText is a markup language and typesetter for math written in ascii art, targeting latex and html (via jtext2latex and jtext2html, resp). One of the coolest features is compiling ascii-art sequent rules to latex.

jtext2latex was used to typeset Fritz Obermeyer's [http://fritzo.org/thesis PhD thesis], which is part of the [http://github.com/fritzo/Johann Johann] theorem prover project. There are lots of examples of .jtext markup in Johann's [https://github.com/fritzo/Johann/tree/master/scripts scripts] directory.