Chris@154: span.cross-ref-title {
Chris@154:  font-size: 140%;
Chris@154: }
Chris@154: span.cross-ref a {
Chris@154:  text-decoration: none;
Chris@154: }
Chris@154: span.cross-ref {
Chris@154:  background-color:#f3f7fa;
Chris@154:  border: 1px dashed #333;
Chris@154:  margin: 1em;
Chris@154:  padding: 0.5em;
Chris@154:  overflow: hidden;
Chris@154: }
Chris@154: a.crossref-toggle {
Chris@154:  text-decoration: none;
Chris@154: }
Chris@154: span.marked0 {
Chris@154:  background-color: rgb(185, 210, 200);
Chris@154:  display: block;
Chris@154: }
Chris@154: span.marked1 {
Chris@154:  background-color: rgb(190, 215, 205);
Chris@154:  display: block;
Chris@154: }
Chris@154: span.inferred0 {
Chris@154:  background-color: rgb(175, 200, 200);
Chris@154:  display: block;
Chris@154: }
Chris@154: span.inferred1 {
Chris@154:  background-color: rgb(180, 205, 205);
Chris@154:  display: block;
Chris@154: }
Chris@154: span.uncovered0 {
Chris@154:  background-color: rgb(225, 110, 110);
Chris@154:  display: block;
Chris@154: }
Chris@154: span.uncovered1 {
Chris@154:  background-color: rgb(235, 120, 120);
Chris@154:  display: block;
Chris@154: }
Chris@154: span.overview {
Chris@154:  border-bottom: 8px solid black;
Chris@154: }
Chris@154: div.overview {
Chris@154:  border-bottom: 8px solid black;
Chris@154: }
Chris@154: #content div.footer {
Chris@154:  font-size: 68%;
Chris@154:  margin-top: 1.5em;
Chris@154: }
Chris@154: #content h1, h2, h3, h4, h5, h6 {
Chris@154:  margin-bottom: 0.5em;
Chris@154: }
Chris@154: h5 {
Chris@154:  margin-top: 0.5em;
Chris@154: }
Chris@154: .hidden {
Chris@154:  display: none;
Chris@154: }
Chris@154: div.separator {
Chris@154:  height: 10px;
Chris@154: }
Chris@154: /* Commented out for better readability, esp. on IE */
Chris@154: /*
Chris@154: table tr td, table tr th {
Chris@154:  font-size: 68%;
Chris@154: }
Chris@154: td.value table tr td {
Chris@154:  font-size: 11px;
Chris@154: }
Chris@154: */
Chris@154: table.percent_graph {
Chris@154:  height: 12px;
Chris@154:  border: #808080 1px solid;
Chris@154:  empty-cells: show;
Chris@154: }
Chris@154: table.percent_graph td.covered {
Chris@154:  height: 10px;
Chris@154:  background: #00f000;
Chris@154: }
Chris@154: table.percent_graph td.uncovered {
Chris@154:  height: 10px;
Chris@154:  background: #e00000;
Chris@154: }
Chris@154: table.percent_graph td.NA {
Chris@154:  height: 10px;
Chris@154:  background: #eaeaea;
Chris@154: }
Chris@154: table.report {
Chris@154:  border-collapse: collapse;
Chris@154:  width: 100%;
Chris@154: }
Chris@154: table.report td.heading {
Chris@154:  background: #dcecff;
Chris@154:  border: #d0d0d0 1px solid;
Chris@154:  font-weight: bold;
Chris@154:  text-align: center;
Chris@154: }
Chris@154: table.report td.heading:hover {
Chris@154:  background: #c0ffc0;
Chris@154: }
Chris@154: table.report td.text {
Chris@154:  border: #d0d0d0 1px solid;
Chris@154: }
Chris@154: table.report td.value,
Chris@154: table.report td.lines_total,
Chris@154: table.report td.lines_code {
Chris@154:  text-align: right;
Chris@154:  border: #d0d0d0 1px solid;
Chris@154: }
Chris@154: table.report tr.light {
Chris@154:  background-color: #f6f7f8;
Chris@154: }
Chris@154: table.report tr.dark {
Chris@154:  background-color: #fff;
Chris@154: }
Chris@154: span.run0 {
Chris@154:   background-color: rgb(178, 204, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run1 {
Chris@154:   background-color: rgb(178, 206, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run2 {
Chris@154:   background-color: rgb(178, 209, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run3 {
Chris@154:   background-color: rgb(178, 211, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run4 {
Chris@154:   background-color: rgb(178, 214, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run5 {
Chris@154:   background-color: rgb(178, 218, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run6 {
Chris@154:   background-color: rgb(178, 220, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run7 {
Chris@154:   background-color: rgb(178, 223, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run8 {
Chris@154:   background-color: rgb(178, 225, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run9 {
Chris@154:   background-color: rgb(178, 228, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run10 {
Chris@154:   background-color: rgb(178, 232, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run11 {
Chris@154:   background-color: rgb(178, 234, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run12 {
Chris@154:   background-color: rgb(178, 237, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run13 {
Chris@154:   background-color: rgb(178, 239, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run14 {
Chris@154:   background-color: rgb(178, 242, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run15 {
Chris@154:   background-color: rgb(178, 246, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run16 {
Chris@154:   background-color: rgb(178, 248, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run17 {
Chris@154:   background-color: rgb(178, 251, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run18 {
Chris@154:   background-color: rgb(178, 253, 255);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run19 {
Chris@154:   background-color: rgb(178, 255, 253);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run20 {
Chris@154:   background-color: rgb(178, 255, 249);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run21 {
Chris@154:   background-color: rgb(178, 255, 247);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run22 {
Chris@154:   background-color: rgb(178, 255, 244);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run23 {
Chris@154:   background-color: rgb(178, 255, 242);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run24 {
Chris@154:   background-color: rgb(178, 255, 239);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run25 {
Chris@154:   background-color: rgb(178, 255, 235);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run26 {
Chris@154:   background-color: rgb(178, 255, 233);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run27 {
Chris@154:   background-color: rgb(178, 255, 230);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run28 {
Chris@154:   background-color: rgb(178, 255, 228);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run29 {
Chris@154:   background-color: rgb(178, 255, 225);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run30 {
Chris@154:   background-color: rgb(178, 255, 221);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run31 {
Chris@154:   background-color: rgb(178, 255, 219);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run32 {
Chris@154:   background-color: rgb(178, 255, 216);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run33 {
Chris@154:   background-color: rgb(178, 255, 214);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run34 {
Chris@154:   background-color: rgb(178, 255, 211);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run35 {
Chris@154:   background-color: rgb(178, 255, 207);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run36 {
Chris@154:   background-color: rgb(178, 255, 205);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run37 {
Chris@154:   background-color: rgb(178, 255, 202);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run38 {
Chris@154:   background-color: rgb(178, 255, 200);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run39 {
Chris@154:   background-color: rgb(178, 255, 197);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run40 {
Chris@154:   background-color: rgb(178, 255, 193);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run41 {
Chris@154:   background-color: rgb(178, 255, 191);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run42 {
Chris@154:   background-color: rgb(178, 255, 188);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run43 {
Chris@154:   background-color: rgb(178, 255, 186);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run44 {
Chris@154:   background-color: rgb(178, 255, 183);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run45 {
Chris@154:   background-color: rgb(178, 255, 179);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run46 {
Chris@154:   background-color: rgb(179, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run47 {
Chris@154:   background-color: rgb(182, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run48 {
Chris@154:   background-color: rgb(184, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run49 {
Chris@154:   background-color: rgb(187, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run50 {
Chris@154:   background-color: rgb(191, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run51 {
Chris@154:   background-color: rgb(193, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run52 {
Chris@154:   background-color: rgb(196, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run53 {
Chris@154:   background-color: rgb(198, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run54 {
Chris@154:   background-color: rgb(201, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run55 {
Chris@154:   background-color: rgb(205, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run56 {
Chris@154:   background-color: rgb(207, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run57 {
Chris@154:   background-color: rgb(210, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run58 {
Chris@154:   background-color: rgb(212, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run59 {
Chris@154:   background-color: rgb(215, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run60 {
Chris@154:   background-color: rgb(219, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run61 {
Chris@154:   background-color: rgb(221, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run62 {
Chris@154:   background-color: rgb(224, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run63 {
Chris@154:   background-color: rgb(226, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run64 {
Chris@154:   background-color: rgb(229, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run65 {
Chris@154:   background-color: rgb(233, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run66 {
Chris@154:   background-color: rgb(235, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run67 {
Chris@154:   background-color: rgb(238, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run68 {
Chris@154:   background-color: rgb(240, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run69 {
Chris@154:   background-color: rgb(243, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run70 {
Chris@154:   background-color: rgb(247, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run71 {
Chris@154:   background-color: rgb(249, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run72 {
Chris@154:   background-color: rgb(252, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run73 {
Chris@154:   background-color: rgb(255, 255, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run74 {
Chris@154:   background-color: rgb(255, 252, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run75 {
Chris@154:   background-color: rgb(255, 248, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run76 {
Chris@154:   background-color: rgb(255, 246, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run77 {
Chris@154:   background-color: rgb(255, 243, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run78 {
Chris@154:   background-color: rgb(255, 240, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run79 {
Chris@154:   background-color: rgb(255, 238, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run80 {
Chris@154:   background-color: rgb(255, 234, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run81 {
Chris@154:   background-color: rgb(255, 232, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run82 {
Chris@154:   background-color: rgb(255, 229, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run83 {
Chris@154:   background-color: rgb(255, 226, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run84 {
Chris@154:   background-color: rgb(255, 224, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run85 {
Chris@154:   background-color: rgb(255, 220, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run86 {
Chris@154:   background-color: rgb(255, 218, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run87 {
Chris@154:   background-color: rgb(255, 215, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run88 {
Chris@154:   background-color: rgb(255, 212, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run89 {
Chris@154:   background-color: rgb(255, 210, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run90 {
Chris@154:   background-color: rgb(255, 206, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run91 {
Chris@154:   background-color: rgb(255, 204, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run92 {
Chris@154:   background-color: rgb(255, 201, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run93 {
Chris@154:   background-color: rgb(255, 198, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run94 {
Chris@154:   background-color: rgb(255, 196, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run95 {
Chris@154:   background-color: rgb(255, 192, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run96 {
Chris@154:   background-color: rgb(255, 189, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run97 {
Chris@154:   background-color: rgb(255, 187, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run98 {
Chris@154:   background-color: rgb(255, 184, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run99 {
Chris@154:   background-color: rgb(255, 182, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: span.run100 {
Chris@154:   background-color: rgb(255, 178, 178);
Chris@154:   display: block;
Chris@154: }
Chris@154: pre {
Chris@154:     white-space: pre-wrap; /* CSS2.1 compliant */
Chris@154:     white-space: -moz-pre-wrap; /* Mozilla-based browsers */
Chris@154:     white-space: -o-pre-wrap; /* Opera 7+ */
Chris@154: }