.nocode { white-space: pre }
.exec   { white-space: pre; background-color: green; color: white;}
.noexec { white-space: pre; background-color: red; color: white;}
.num    { text-align: right; }
.summary_header { border: black solid 1px; margin-top: 2em; }
.shade-row { background-color: #cccccc; }