/* copyright 2006 MJRoberts */
/* style sheet for TADS 3 Library Reference Manual */

body {
    font: 10pt/14pt Verdana, Arial, Helvetica, Sans-Serif;
    background: #ffffff;
    color: #000000;
}

table {
    font: 10pt/14pt Verdana, Arial, Helvetica, Sans-Serif;
}

a {
    text-decoration: none;
}

a:hover {
    text-decoration: underline;
}

h1 {
    font-size: 150%;
    font-weight: normal;
    color: #000080;
}

h2 {
    font-size: 125%;
    font-weight: normal;
    color: #000080;
}

h3 {
    font-size: 110%; 
    font-weight: normal;
    color: #000080;
}

h4 {
    font-size: 100%; 
    font-weight: bold;
    color: #000080;
}

div.mjhd {
    width: 100%;
    padding-left: 5px;
    padding-right: 5px;
    padding-top: 0px;
    padding-bottom: 0px;
    color: #000080;
    background: #d0d0d0;
}

span.hdln {
    font-size: 133%;
}

span.title {
    font-size: 150%;
    line-height: 200%;
    color: #000080;
}
span.type {
    font-size: 80%;
    font-style: italic;
    color: #000080;
    margin-left: 1.5em;
}

table.ban {
    width: 100%;
}
table.ban tr {
    vertical-align: middle;
}
table.ban td {
    padding: 0px;
}

table.hdr {
    width: 100%;
}
table.hdr tr {
    vertical-align: middle;
}
table.hdr td {
    padding: 0px;
    text-align: center;
}

table.nav {
    width: 100%;
}
table.nav tr {
    vertical-align: middle;
    background: #f0f0f0;
}
table.nav td {
    padding: 0px 0.5em 0px 0.5em;
    text-align: center;
    background: #e0e0e0;
}

table.decl {
    width: 100%;
}
table.decl tr {
    vertical-align: top;
}
table.decl td {
    padding: 0px;
}
table.decl td code {
    font-family: 9pt/12pt Courier New, Courier, monospace;
}
span.rem {
    font-family: default;
    font-style: italic;
    padding-left: 1.5em;
}
span.gramalt {
    font-weight: 600;
}
span.classExtLink {
    font-weight: 600;
}

div.fdesc {
    margin: 1em 0px 1em 0px;
}

div.desc {
    margin-left: 2.5em;
    margin-bottom: 1em;
}

div.gramrule {
    margin-left: 2.5em;
    margin-bottom: 1em;
    font-family: Courier New, Courier, monospace;
    font-size: 80%;
}

span.code {
    font-family: Courier New, Courier, monospace;
    color: #000080;
}

div.fdef {
    margin-left: 3em;
    margin-top: 0.5em;
    margin-bottom: 2em;
}

div.ftr {
    border-top: 3px solid #d0d0d0;
    margin-top: 5em;
    padding-top: 5px;
    font-style: italic;
    color: #606060;
}