li, td, th {
    font-size: small;
    vertical-align: top;
    text-align: left;
}

th {
    font-weight: bold;
    text-align: center;
}

caption {
    caption-side: top;
    width: auto;
    text-align: left;
    font-weight: bold;
    color: rgb(0, 0, 153);
    background-color: rgb(204, 204, 204);
}

#keyword {
    font-weight: bold;
    color: rgb(0, 0, 153);
}

.tiny {
    font-size: xx-small;
    text-align: right;
}

.nx {
    font-weight: bold;
}

.nx, a:hover.nx, a:link.nx, a:visited.nx {
    color: #009933;
    text-decoration: none;
}

.nxf {
    font-weight: bold;
}

.nxf, a:hover.nxf, a:link.nxf, a:visited.nxf {
    color: purple;
    text-decoration: none;
}

#yellow, #redOnYellow {
    background-color: rgb(255, 255, 153);
}

#redOnYellow {
    color: red;
    font-weight: bold;
}

#grayTable, #grayTable_indent {
    text-align: left;
    background-color: rgb(204, 204, 204);
    margin-left: 40px;
    width: 80%;
}

#grayTable_indent {
    text-align: left;
    background-color: rgb(204, 204, 204);
    margin-left: 80px;
}

.lindent {
    margin-left: 20px;
}

#darkGray {
    background-color: rgb(192, 192, 192);
}

.field, .field_indent, .field_indent_indent, .field_name {
    font-size: medium;
    font-weight: bold;
    margin-bottom: 10px
}

.field_indent {
    margin-left: 40px;
}

.field_indent_indent {
    margin-left: 80px;
}

.field_name {
    font-style: italic;
    color: purple;
}

.field_desc, .field_desc_indent, .field_explain, .field_simple {
    font-size: small;
    margin-bottom: 10px
}

.field_explain {
    border-width: 1px 1px 1px 1px;
    border-style: outset;
    padding-left: 3px;
    padding-right: 3px;
    padding-bottom: 3px;
    padding-top: 3px;
}

.field_desc, .field_desc_indent {
    margin-left: 40px;
}

.field_desc_indent {
    margin-left: 80px;
}

.cpp, .cpp_comment {
    font-size: medium;
    font-family: monospace;
    background-color: rgb(255, 255, 204);
    margin-left: 40px;
}

.cpp_comment {
    color: #3333FF;
}

.copyright {
    text-align: center;
    background-color: rgb(153, 153, 153);
    color: #COCOCO;
}