Better CSS styling options ensue, if we put the class='lang' on the <pre> element. (Suggested by Casper Gripenberg)