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