.plain         { }
.doc           { color: rgb(  0,   0,   0); }
.frame         { color: rgb(255,   0,   0); }
.type          { color: rgb(  0,  58,   0); }
.type_mod      { color: rgb(  0,  80,   0); }
.result        { color: rgb(  0,  58,   0); }
.result_mod    { color: rgb(  0,  80,   0); }
.class         { color: rgb(180,   0, 180); }
.defval        { color: rgb(180,   0,   0); }
.functor       { color: rgb(  0,   0, 180); }
.label         { color: rgb(255,   0,   0); }
.highlight     { color: rgb(200,  58,   0); }
.ifdef {
    color: rgb(0, 90, 30);
    font-family: Courier, Courier-New, typewriter, monospace;
}
.code {
    color: rgb(  0,   0,   0);
    background-color: rgb(216, 216, 216);
    border: 1px solid black;
    padding: 5px;
    margin-left:  3em;
    margin-right: 3em;
    white-space: pre;
}
.namespace     { background-color: rgb(216, 216, 255); }
.abstract      { background-color: rgb(255, 216, 216); }
.concrete      { background-color: rgb(216, 255, 216); }
.hnormal      {
    background-color: rgb(216, 216, 216);
    padding-top:      1ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.honormal     {
    background-color: rgb(216, 216, 216);
    padding-top:      1ex;
    padding-bottom:   0.5ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.hunormal     {
    background-color: rgb(216, 216, 216);
    padding-top:      0.5ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.divnormal    {
    background-color: rgb(216, 216, 216);
    border: 1px solid black;
    width:            90%;
    padding-left:     0ex;
    padding-right:    0ex;
    padding-top:      0ex;
    padding-bottom:   0ex;
    margin-left:      0em;
    margin-right:     0em;
    margin-top:       1ex;
    margin-bottom:    1ex;
}
.honamespace  {
    background-color: rgb(216, 216, 255);
    padding-top:      1ex;
    padding-bottom:   0.5ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.hunamespace  {
    background-color: rgb(216, 216, 255);
    padding-top:      0.5ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.divnamespace {
    background-color: rgb(216, 216, 255);
    border: 1px solid black;
    width:            90%;
    padding-left:     0ex;
    padding-right:    0ex;
    padding-top:      0ex;
    padding-bottom:   0ex;
    margin-left:      0em;
    margin-right:     0em;
    margin-top:       1ex;
    margin-bottom:    1ex;
}
.hoabstract   {
    background-color: rgb(255, 216, 216);
    padding-top:      1ex;
    padding-bottom:   0.5ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.huabstract   {
    background-color: rgb(255, 216, 216);
    padding-top:      0.5ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.divabstract  {
    background-color: rgb(255, 216, 216);
    border: 1px solid black;
    width:            90%;
    padding-left:     0ex;
    padding-right:    0ex;
    padding-top:      0ex;
    padding-bottom:   0ex;
    margin-left:      0em;
    margin-right:     0em;
    margin-top:       1ex;
    margin-bottom:    1ex;
}
.hoconcrete   {
    background-color: rgb(216, 255, 216);
    padding-top:      1ex;
    padding-bottom:   0.5ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.huconcrete   {
    background-color: rgb(216, 255, 216);
    padding-top:      0.5ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.divconcrete  {
    background-color: rgb(216, 255, 216);
    border: 1px solid black;
    width:            90%;
    padding-left:     0ex;
    padding-right:    0ex;
    padding-top:      0ex;
    padding-bottom:   0ex;
    margin-left:      0em;
    margin-right:     0em;
    margin-top:       1ex;
    margin-bottom:    1ex;
}
.hfunctions   {
    background-color: rgb(216, 255, 255);
    padding-top:      1ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.divfunctions {
    background-color: rgb(216, 255, 255);
    border: 1px solid black;
    width:            90%;
    padding-left:     0ex;
    padding-right:    0ex;
    padding-top:      0ex;
    padding-bottom:   0ex;
    margin-left:      0em;
    margin-right:     0em;
    margin-top:       1ex;
    margin-bottom:    1ex;
}
td,th,tr {
   padding-left:   0.3em;
   padding-right:  0.3em;
   padding-top:    0pt;
   padding-bottom: 0pt;
}
td.normalsyn  { background-color: rgb(192,192,192); }
td.leftsyn    { background-color: rgb(192,192,192); }
td.rightsyn   { background-color: rgb(192,192,192); }
td.centersyn  { background-color: rgb(192,192,192); }
table.nullfullsyn   { background-color: rgb(192,192,192); }
table.nullcentersyn { background-color: rgb(192,192,192); }
.syn {
    background-color: rgb(192,192,192);
    font-family: Courier, Courier-New, typewriter, monospace;
}
.syncode {
    background-color: rgb(192,192,192);
    font-family: Courier, Courier-New, typewriter, monospace;
    border: 1px solid black;
    padding: 5px;
    margin-left:  3em;
    margin-right: 3em;
    white-space: pre;
}
.synH1 {
    background-color: rgb(255, 255, 255);
    padding-top:      1ex;
    padding-bottom:   1ex;
    padding-left:     0ex;
    padding-right:    0ex;
    margin:           0px;
}
.synHead {
    background-color: rgb(255, 255, 255);
    border: 1px solid black;
    width:            90%;
    padding-left:     0ex;
    padding-right:    0ex;
    padding-top:      0ex;
    padding-bottom:   0ex;
    margin-left:      0em;
    margin-right:     0em;
    margin-top:       1ex;
    margin-bottom:    1ex;
}
.synLine {
    background-color: rgb(192,192,192);
    color: rgb(  0, 0, 180);
    font-weight: normal;
}
.synLineHot {
    background-color: rgb(192,192,192);
    color: rgb(100, 0, 220);
    font-weight: bold;
}
.synSpace          { background-color: rgb(192,192,192);                          }
.synIdent          { background-color: rgb(192,192,192); color: rgb(  0,   0,   0);                   }
.synIdentLink      { background-color: rgb(192,192,192); color: rgb(  0,   0,   0);             text-decoration: underline; }
.synResStatic      { background-color: rgb(192,192,192); color: rgb(127, 127,   0);  font-weight: bold;       }
.synResStaticLink  { background-color: rgb(192,192,192); color: rgb(127, 127,   0);  font-weight: bold; text-decoration: underline; }
.synResConst       { background-color: rgb(192,192,192); color: rgb(127, 127,   0);  font-weight: bold;       }
.synResConstLink   { background-color: rgb(192,192,192); color: rgb(127, 127,   0);  font-weight: bold; text-decoration: underline; }
.synResPublic      { background-color: rgb(192,192,192); color: rgb(127,   0, 127); font-weight: bold;       }
.synResPublicLink  { background-color: rgb(192,192,192); color: rgb(127,   0, 127); font-weight: bold; text-decoration: underline; }
.synResInt         { background-color: rgb(192,192,192); color: rgb(  0, 100,   0);   font-weight: normal;       }
.synResIntLink     { background-color: rgb(192,192,192); color: rgb(  0, 100,   0);   font-weight: normal; text-decoration: underline; }
.synResIf          { background-color: rgb(192,192,192); color: rgb(127,   0, 127); font-weight: bold;       }
.synResIfLink      { background-color: rgb(192,192,192); color: rgb(127,   0, 127); font-weight: bold; text-decoration: underline; }
.synResAssert      { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold;       }
.synResAssertLink  { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold; text-decoration: underline; }
.synPreProc        { background-color: rgb(192,192,192); color: rgb(127, 127,   0);  font-weight: bold;       }
.synPreProcLink    { background-color: rgb(192,192,192); color: rgb(127, 127,   0);  font-weight: bold; text-decoration: underline; }
.synInt            { background-color: rgb(192,192,192); color: rgb(  0,   0,   0);                   }
.synIntLink        { background-color: rgb(192,192,192); color: rgb(  0,   0,   0);             text-decoration: underline; }
.synOp             { background-color: rgb(192,192,192); color: rgb(  0,   0, 100);    font-weight: bold;       }
.synOther          { background-color: rgb(192,192,192); color: rgb(  0,   0, 100);    font-weight: bold;       }
.synFloat          { background-color: rgb(192,192,192); color: rgb(  0,   0,   0);                   }
.synFloatLink      { background-color: rgb(192,192,192); color: rgb(  0,   0,   0);             text-decoration: underline; }
.synHotComment     { background-color: rgb(192,192,192); color: rgb(255, 255, 127); font-weight: bold;       }
.synHotCxxComment  { background-color: rgb(192,192,192); color: rgb(255, 255, 127); font-weight: bold;       }
.synHotCommentLink { background-color: rgb(192,192,192); color: rgb(255, 255, 127); font-weight: bold; text-decoration: underline; }
.synCxxComment     { background-color: rgb(192,192,192); color: rgb(255, 255, 255);       font-weight: bold;       }
.synCxxCommentLink { background-color: rgb(192,192,192); color: rgb(255, 255, 255);       font-weight: bold; text-decoration: underline; }
.synComment        { background-color: rgb(192,192,192); color: rgb(255, 255, 255);       font-weight: bold;       }
.synCommentLink    { background-color: rgb(192,192,192); color: rgb(255, 255, 255);       font-weight: bold; text-decoration: underline; }
.synCommentERR     { background-color: rgb(192,192,192); color: rgb(255,   0,   0);    font-weight: bold;       }
.synSymbol         { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold;       }
.synSymbolLink     { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold; text-decoration: underline; }
.synString         { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold;       }
.synStringLink     { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold; text-decoration: underline; }
.synStringERR      { background-color: rgb(192,192,192); color: rgb(255,   0,   0);    font-weight: bold;       }
.synChar           { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold;       }
.synCharLink       { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold; text-decoration: underline; }
.synCharERR        { background-color: rgb(192,192,192); color: rgb(255,   0,   0);    font-weight: bold;       }
.synBackslashCR    { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold;       }
.synBackslashOther { background-color: rgb(192,192,192); color: rgb(210,   0,   0);     font-weight: bold;       }
.synOther          { background-color: rgb(192,192,192); color: rgb(  0, 100,   0);   font-weight: normal;       }