Text.PrettyPrint.HughesPJ inserting blank lines
maeder at tzi.de
Wed Jan 26 13:51:27 EST 2005
I've found myself using "$+$ space $+$" in order to insert a blank line
between two docs.
There are probably other ways to do it. "(test "")" (and $$) instead of
"space" (or $+$) also work in many cases (but not "empty"). Which way
would be the best?
Maybe one could add a further function "$++$" to do this and a list
version "vsep" of "$++$"?
Another idea might be something like a vertical space "vspace" so that
several blank lines would be created by: $$ vspace $$ vspace $$ ...
More information about the Libraries