1/* CSS specific to the live ranges div associated with 2 the RangeView typescript class in src/range-view.ts. */ 3 4:root { 5 --range-y-axis-width: 18ch; 6 --range-position-width: 3.5ch; 7 --range-block-border: 6px; 8 --range-instr-border: 3px; 9 --range-position-border: 1px; 10} 11 12.range-bold { 13 font-weight: bold; 14 color: black; 15} 16 17#ranges { 18 font-family: monospace; 19 min-height: auto; 20 overflow: hidden; 21} 22 23#resizer-ranges { 24 height: 10px; 25} 26 27.range-title-div { 28 padding: 2ch 2ch 2ch 2ch; 29 white-space: nowrap; 30 overflow: auto; 31} 32 33.range-title { 34 text-decoration: underline; 35 font-weight: bold; 36 font-size: large; 37 display: inline-block; 38} 39 40.range-title-help { 41 margin-left: 2ch; 42 width: 1ch; 43 padding: 0 0.25ch; 44 border: 1px dotted black; 45 color: slategray; 46 display: inline-block; 47} 48 49input.range-toggle-show { 50 vertical-align: middle; 51} 52 53.range-header-label-x { 54 text-align: center; 55 margin-left: 13ch; 56} 57 58.range-header-label-y { 59 width: 11ch; 60 float: left; 61 white-space: pre-wrap; 62 word-wrap: break-word; 63 margin-left: 6ch; 64 margin-top: 4ch; 65} 66 67.range-y-axis { 68 display: inline-block; 69 width: var(--range-y-axis-width); 70 overflow: hidden; 71 white-space: nowrap; 72 vertical-align: top; 73} 74 75.range-header { 76 display: flex; 77 overflow: hidden; 78 height: 8ch; 79 margin-left: var(--range-y-axis-width); 80} 81 82.range-position-labels, 83.range-register-labels { 84 background-color: lightgray; 85} 86 87.range-register-labels { 88 float: right; 89} 90 91.range-position-labels { 92 margin-top: auto; 93} 94 95.range-registers { 96 float: right; 97 overflow: hidden; 98 text-align: right; 99} 100 101.range-positions-header, 102.range-instruction-ids, 103.range-block-ids { 104 overflow: hidden; 105 white-space: nowrap; 106 display: grid; 107 grid-gap: 0; 108} 109 110.range-reg { 111 width: 13ch; 112 text-align: right; 113} 114 115.range-reg::after { 116 content: ":"; 117} 118 119.range-grid { 120 overflow: auto; 121 display: inline-block; 122 white-space: nowrap; 123} 124 125.range-block-id { 126 display: inline-block; 127 text-align: center; 128} 129 130.range-instruction-id { 131 display: inline-block; 132 text-align: center; 133} 134 135.range-position { 136 display: inline-block; 137 text-align: center; 138 z-index: 1; 139} 140 141.range-transparent, 142.range-position.range-empty { 143 color: transparent; 144} 145 146.range-block-id:hover, 147.range-instruction-id:hover, 148.range-reg:hover, 149.range-position:hover { 150 background-color: rgba(0, 0, 255, 0.10); 151} 152 153.range-position.range-header-element { 154 border-bottom: 2px solid rgb(109, 107, 107); 155} 156 157.range-block-id, 158.range-instruction-id, 159.range-reg, 160.range-interval, 161.range-position { 162 position: relative; 163 border: var(--range-position-border) solid rgb(109, 107, 107); 164} 165 166.range-block-id, 167.range-instruction-id, 168.range-interval, 169.range-position { 170 border-left: 0; 171} 172 173.range-block-ids > .range-block-id:first-child, 174.range-instruction-ids > .range-instruction-id:first-child, 175.range-positions > .range-position:first-child { 176 border-left: var(--range-position-border) solid rgb(109, 107, 107); 177} 178 179.range-position.range-interval-position { 180 border: none; 181} 182 183.range-interval-text { 184 position: absolute; 185 padding-left: 0.5ch; 186 z-index: 2; 187 pointer-events: none 188} 189 190.range-position.range-use { 191 border-left: var(--range-instr-border) solid red; 192} 193 194.range-block-border, 195.range-block-border.range-position.range-interval-position:last-child { 196 border-right: var(--range-block-border) solid rgb(109, 107, 107); 197} 198 199.range-block-border.range-position.range-interval-position { 200 border-right: var(--range-block-border) solid transparent; 201} 202 203.range-instr-border, 204.range-instr-border.range-position.range-interval-position:last-child { 205 border-right: var(--range-instr-border) solid rgb(109, 107, 107); 206} 207 208.range-instr-border.range-position.range-interval-position { 209 border-right: var(--range-instr-border) solid transparent; 210} 211 212.range, 213.range-interval, 214.range-interval-wrapper, 215.range-positions { 216 white-space: nowrap; 217 display: inline-block; 218} 219 220.range-interval-wrapper, 221.range-positions { 222 display: grid; 223 grid-gap: 0; 224} 225 226.range-interval { 227 background-color: rgb(153, 158, 168); 228} 229 230.range-hidden { 231 display: none !important; 232} 233 234.range-positions-placeholder { 235 width: 100%; 236 border: var(--range-position-border) solid transparent; 237 color: transparent; 238}