div.pseudo {
    white-space: pre;
    padding: 0px;
    margin: 0px;
}

div.pseudo span {
    padding: 0px;
    margin: 0px;
}

div.pseudo span.symbol {
    font-weight: bold;
}

div.pseudo span.function {
    font-variant: small-caps;
}

/*
div.pseudo span.op {
    font-family: monospace;
}
*/