body {
    font-family:arial;
    font-size: 0.9em;
}

.filter_row {
    background-color: #eee;
    border: 1px solid black;
    padding: 1em;
}

.code {
    font-family:monospace;
    width: 20%;
    padding: 1em;
}

.inline_code {
    font-family:monospace;
    width: 20%;
}

.menu {
    background-color:#EBEFF9;
    width: 100%;
    list-style: none;
    height: 37px;
    padding-left: 3px;
    padding-top: 2px;
    margin: 0;
}

.menu li {
    display: inline-block;
    vertical-align: middle;
    padding-left: 0;
}

.menu a {
    display: block;
    padding-left: 1em;
}

td.before, td.after {
    padding-left: 1em;
    width: 10%;
}

#pname {
    font-size: 200%;
    margin: 0;
    padding: 0;
}