body { color: #000000; background: #ffffff;
margin: 0px 0px 0px 10px;
padding: 0px 0px 0px 0px;
width: auto;
}
h1 {color: #000000; font-weight: bold; background-color: #FFFFFF;
border-style: solid; border-color: #C0C0FF; border-width: 0px 0px 2px 2px;
margin: 4px 0px 4px 0px;
padding: 8px 2px 8px 2px;
font-size: large;
}
h1.manual {color: #000000; font-weight: bold; background-color: #C0FFC0;
border-style: none; border-width: 1px 1px 1px 1px;
margin: 4px 0px 4px 0px;
padding: 8px 2px 8px 2px;
font-size: large;
}
h2 {color: #000000; font-weight: bold; background-color: #FFFFFF;
border-style: solid; border-color: #C0C0FF; border-width: 0px 0px 2px 2px;
margin: 2px 0px 2px 10px;
padding: 4px 2px 4px 2px;
font-size: large;
}
h2.manual {color: #000000; font-weight: bold; background-color: #FFFFFF;
border-style: solid; border-width: 0px 0px 3px 10px;
border-color: #C0FFC0;
margin: 2px 0px 2px 0px;
padding: 16px 2px 4px 2px;
width: 500px;
font-size: large;
}
h3.manual {color: #000000; font-weight: bold; background-color: #FFFFFF;
border-style: solid; border-width: 0px 0px 3px 30px;
border-color: #C0FFC0;
margin: 2px 0px 2px 0px;
padding: 16px 2px 4px 2px;
width: 500px;
font-size: medium;
}
div.plain {
color: #000000; background: #F0F0FF;
border-style: none; border-width: 1px 1px 1px 1px;
margin: 6px 0px 6px 24px;
padding: 4px 0px 4px 0px;
width: 70%;
}
div.exec {
color: #000000; background: #F0F0F0;
border-style: solid; border-width: 1px 1px 1px 1px;
margin: 12px 0px 12px 24px;
padding: 2px 6px 2px 6px;
width: 500px;
}
div.warning {
color: #000000; background: #FFE0E0;
border-style: none; border-width: 1px 1px 1px 1px;
margin: 6px 0px 6px 24px;
padding: 4px 0px 4px 0px;
width: 500px;
}
div.hint {
color: #000000; background: #FFFFCF;
border-style: solid; border-width: 1px 1px 1px 1px;
margin: 12px 0px 12px 24px;
padding: 2px 12px 2px 12px;
width: 60%;
}
div.highlight {
color: #000000; background: #FFFFCF;
border-style: solid; border-width: 1px 1px 1px 1px;
margin: 12px 0px 12px 24px;
padding: 2px 12px 2px 12px;
width: 500px;
}
div.exercise {
color: #000000; background: #FFFFFF;
border-style: none; border-width: 0px 0px 0px 0px;
margin: 2px 0px 2px 0px;
padding: 2px 2px 2px 2px;
width: 600px;
}
span.warning {
color: #000000; background: #FF8080;
}
pre.source {
color: #000000; background: #EEEEEE;
border-style: solid; border-width: 1px 1px 1px 1px;
margin: 12px 24px 12px 24px;
padding: 2px 6px 0px 6px;
width: auto;
font-size: medium;
font-family: courier ,monospace;
}
table.syntaxlist {
color: #000000; background: #D0D0FF;
border-style: solid; border-width: 2px 2px 2px 2px;
border-color: #9F9FFF;
text-align: center;
}
thead.syntaxlist {
color: #000000; background: #E0E0FF;
}
th.syntaxlist {
margin: 12px 0px 12px 0px;
padding: 3px 60px 3px 60px;
}
p {
color: #000000; background: #FFFFFF;
border-style: none; border-width: 1px 1px 1px 1px;
margin: 6px 0px 6px 12px;
padding: 4px 0px 4px 0px;
width: 500px;
}
tr.highest {
background: #F0F0FF;
}
tr.high {
background: #D7D7FF;
}
tr.middle {
background: #B0B0FF;
}
tr.low {
background: #9090FF;
}
a {
text-decoration: none;
}