1// http://stackoverflow.com/questions/71074/how-to-remove-firefoxs-dotted-outline-on-buttons-as-well-as-links/3844452#3844452 2:focus { 3 outline: none; 4} 5::-moz-focus-inner { 6 border: 0; 7} 8 9@keyframes pulsate { 10 from { opacity: 1; } 11 to { opacity: 0.25; } 12} 13 14#part-header { 15 background: #444444; 16 color: #ffffff; 17 font: 24pt monospace; 18 border-bottom: 2px solid #cccccc; 19 padding: 20px 0px 20px 10px; 20} 21 22/* http://css-tricks.com/snippets/css/a-guide-to-flexbox/ */ 23#part-middle { 24 display: flex; 25 flex-direction: row; 26 flex-wrap: nowrap; 27 justify-content: space-between; 28 align-items: stretch; 29 align-content: stretch; 30 31 min-height: 800px; 32 33 border-top: 1px solid #ffffff; 34 padding: 8px; 35 margin-top: 2px; 36} 37#left-area { 38 flex: 0 0 11em; 39 margin-right: 20px; 40 margin-bottom: 10px; 41} 42#center-area { 43 flex: 1 1 0; 44 margin-bottom: 10px; 45} 46#right-area { 47 flex: 0 0 40em; 48 margin-left: 20px; 49 margin-bottom: 10px; 50} 51 52#part-footer { 53 clear: both; 54 border-top: 2px solid #bbbbbb; 55 background: #eeeeee; 56 color: #555555; 57 text-align: center; 58 padding-top: 12px; 59 padding-bottom: 12px; 60 line-height: 1.5; 61} 62 63#exec-status { 64 margin-top: 25px; 65 margin-bottom: 25px; 66} 67#exec-state { 68 display: inline-block; 69 vertical-align: middle; 70} 71#exec-other { 72 display: inline-block; 73 vertical-align: middle; 74 font-size: 125%; 75} 76#current-state { 77 background: #228822; 78 color: #ffffff; 79 font: 16pt; 80 padding: 6pt; 81 border: 5px solid #228822; 82 border-radius: 10px; 83 font-size: 200%; 84 font-weight: bold; 85 margin-right: 10px; 86} 87#current-state.notrunning { 88 background: #882222; 89 border: 5px solid #882222; 90 border-radius: 10px; 91 animation: pulsate 0.7s cubic-bezier(0.75, 0, 0.75, 1) infinite alternate; 92} 93#exec-other:hover { 94 text-decoration: underline; 95 color: #9999ff; 96} 97 98#left-area button { 99 display: inline-block; 100 width: 100%; 101 min-width: 8em; 102 background: #226622; 103 color: #ffffff; 104 font: 16pt sans-serif; 105 font-weight: bold; 106 text-decoration: none; 107 margin: 10px 0 0 0; 108 padding: 0.4em; 109 border: 2px solid #000000; 110 border-radius: 4px; 111} 112#left-area button a { 113 color: #ffffff; 114 text-decoration: none; 115} 116#left-area button:hover { 117 background: #55aa55; 118} 119#left-area button:disabled { 120 background: #555555; 121 color: #888888; 122} 123#left-area button:disabled a { 124 background: #555555; 125 color: #888888; 126} 127 128#pause-button.pending { 129 background: #5555ff; 130 animation: pulsate 0.2s cubic-bezier(0.75, 0, 0.75, 1) infinite alternate; 131} 132 133#attach-button { 134} 135#attach-button.enabled { 136 animation: pulsate 0.7s cubic-bezier(0.75, 0, 0.75, 1) infinite alternate; 137} 138 139.duktape-exec-line { 140 outline: 2px solid red; 141 background: #550000; 142} 143.duktape-break-line { 144 outline: 2px solid white; 145} 146 147#output { 148 font: 9pt monospace; 149 color: #000000; 150 border: 2px solid #cccccc; 151 border-radius: 5px; 152 padding: 3px; 153 height: 30ex; 154 overflow: scroll; 155 overflow-x: auto; 156 overflow-y: scroll; 157 white-space: pre; 158} 159#output .alert { 160 color: #ff0000; 161} 162/* Default color (should be overridden by level) */ 163#output .log { 164 color: #00ff00; 165} 166/* Trace */ 167#output .loglevel0 { 168 color: #cccccc; 169} 170/* Debug */ 171#output .loglevel1 { 172 color: #cccccc; 173} 174/* Info */ 175#output .loglevel2 { 176 color: #888888; 177 font-weight: bold; 178} 179/* Warn */ 180#output .loglevel3 { 181 color: #ff4444; 182 font-weight: bold; 183} 184/* Error */ 185#output .loglevel4 { 186 color: #ff0000; 187 font-weight: bold; 188} 189/* Fatal */ 190#output .loglevel5 { 191 background: #000000; 192 color: #ff0000; 193 font-weight: bold; 194} 195#output .debugger-info { 196 color: #880000; 197 font-weight: bold; 198 font-style: italic; 199} 200#output .debugger-debug { 201 color: #888888; 202 font-weight: bold; 203 font-style: italic; 204} 205 206#callstack { 207 font: 9pt monospace; 208 color: #000000; 209 margin-top: 10px; 210 border: 2px solid #cccccc; 211 border-radius: 5px; 212 padding: 3px; 213 height: 14ex; 214 overflow: scroll; 215 overflow-x: auto; 216 overflow-y: scroll; 217 white-space: pre; 218} 219#callstack div:nth-child(2n) { 220 background: #eeeeee; 221} 222#callstack .func { 223} 224#callstack .rest { 225 float: right; 226 color: #6666ff; 227} 228#callstack .rest:hover { 229 text-decoration: underline; 230 color: #9999ff; 231} 232 233#locals { 234 font: 9pt monospace; 235 color: #000000; 236 margin-top: 10px; 237 border: 2px solid #cccccc; 238 border-radius: 5px; 239 padding: 10px; 240 height: 30ex; 241 overflow: scroll; 242 overflow-x: auto; 243 overflow-y: scroll; 244 white-space: pre; 245} 246#locals div:nth-child(2n) { 247 background: #eeeeee; 248} 249#locals .key { 250} 251#locals .value { 252 float: right; 253 color: #888888; 254} 255 256#breakpoints { 257 color: #000000; 258 margin-top: 10px; 259 border: 2px solid #cccccc; 260 border-radius: 5px; 261 padding: 3px; 262 height: 15ex; 263 overflow: scroll; 264 overflow-x: auto; 265 overflow-y: scroll; 266 white-space: pre; 267} 268#breakpoints div { 269 margin: 2px 0 2px 0; 270} 271#breakpoints div:nth-child(2n) { 272 background: #eeeeee; 273} 274#breakpoints a { 275 font: 9pt monospace; 276 color: #6666ff; 277} 278#breakpoints a:hover { 279 text-decoration: underline; 280 color: #9999ff; 281} 282.breakpoint-line { 283 clear: both; 284 padding-top: 2px; 285 padding-bottom: 2px; 286} 287#add-breakpoint-file { 288 font: 10pt monospace; 289 width: 10em; 290 padding: 5px; 291} 292#add-breakpoint-line { 293 font: 10pt monospace; 294 width: 3em; 295 margin-left: 3px; 296 padding: 5px; 297} 298#delete-all-breakpoints-button { 299 float: right; 300 font: 10pt sans-serif; 301 padding: 5px; 302 border: 1px solid #888888; 303 background: #ddffdd; 304 color: #000000; 305} 306#delete-all-breakpoints-button:hover { 307 background: #f8fff8; 308} 309#delete-all-breakpoints-button:disabled { 310 background: #dddddd; 311 color: #444444; 312} 313#add-breakpoint-button { 314 font: 10pt sans-serif; 315 margin-left: 10px; 316 padding: 5px; 317 border: 1px solid #888888; 318 background: #ddffdd; 319 color: #000000; 320} 321#add-breakpoint-button:hover { 322 background: #f8fff8; 323} 324#add-breakpoint-button:disabled { 325 background: #dddddd; 326 color: #444444; 327} 328#breakpoint-hint { 329 color: #aaaaaa; 330 font-style: italic; 331 margin-left: 10px; 332} 333.delete-breakpoint-button { 334 float: right; 335 display: inline; 336 font: 9pt sans-serif; 337 padding: 3px; 338 border: none; 339 background: none; 340 color: #6666ff; 341} 342.delete-breakpoint-button { 343 font: 9pt sans-serif; 344} 345.delete-breakpoint-button:hover { 346 text-decoration: underline; 347 color: #9999ff; 348} 349.delete-breakpoint-button:disabled { 350 color: #888888; 351} 352 353#about-dialog p { 354 margin: 10px 0 10px 0; 355} 356 357#bytecode-dialog p { 358 margin: 10px 0 10px 0; 359} 360#bytecode-dialog pre { 361 font: 10pt monospace; 362 color: #000000; 363} 364#bytecode-dialog div.highlight { 365 background: #888888; 366 color: #ffffff; 367} 368 369#eval { 370 color: #000000; 371 margin-top: 10px; 372 border: 2px solid #cccccc; 373 border-radius: 5px; 374 padding: 3px; 375 height: 30ex; 376 overflow: scroll; 377 overflow-x: auto; 378 overflow-y: scroll; 379 white-space: pre; 380} 381#eval-input { 382 display: inline; 383 font: 10pt monospace; 384 width: 20em; 385 padding: 5px; 386} 387#eval-button { 388 display: inline; 389 margin-left: 10px; 390 padding: 5px; 391 border: 1px solid #888888; 392 font: 10pt sans-serif; 393 background: #ddffdd; 394 color: #000000; 395} 396#eval-button { 397} 398#eval-button:hover { 399 background: #f8fff8; 400} 401#eval-button:disabled { 402 background: #dddddd; 403 color: #444444; 404} 405#eval-button.pending { 406 background: #5555ff; 407 animation: pulsate 0.2s cubic-bezier(0.75, 0, 0.75, 1) infinite alternate; 408} 409#eval-watch { 410 margin-left: 20px; 411 vertical-align: middle; 412} 413#eval-output { 414 font: 10pt monospace; 415 white-space: pre; 416 padding: 5px; 417 border: 1px solid #888888; 418 min-height: 4ex; 419 margin-top: 5px; 420} 421 422#varname-input { 423 font: 10pt monospace; 424 width: 10em; 425 padding: 5px; 426} 427#varvalue-input { 428 margin-left: 10px; 429 font: 10pt monospace; 430 width: 20em; 431 padding: 5px; 432} 433#getvar-button, 434#putvar-button { 435 display: inline; 436 float: right; 437 margin-left: 10px; 438 padding: 5px; 439 border: 1px solid #888888; 440 font: 10pt sans-serif; 441 background: #ddffdd; 442 color: #000000; 443} 444#getvar-button:hover, 445#putvar-button:hover { 446 background: #f8fff8; 447} 448#getvar-button:disabled, 449#putvar-button:disabled { 450 background: #dddddd; 451 color: #444444; 452} 453#var-output { 454 font: 10pt monospace; 455 white-space: pre; 456 padding: 5px; 457 border: 1px solid #888888; 458 min-height: 4ex; 459 margin-top: 5px; 460} 461 462#source-pre { 463 margin-top: 10px; 464 border: 2px solid #cccccc; 465 border-radius: 5px; 466 height: 400px; 467 overflow: scroll; 468 overflow-x: auto; 469 overflow-y: scroll; 470} 471#source-pre.running { 472 background: #eeeeee; 473 color: #888888; 474} 475#source-pre.running #source-code { 476 background: #eeeeee; 477 color: #888888; 478} 479#source-filename { 480 font-size: 125%; 481 color: #888888; 482} 483code.sourcecode { 484 counter-reset: source-line; 485} 486code.sourcecode div { 487 font: 10pt monospace; 488 padding: 2px 5px 2px 5px; 489 white-space: pre; 490 border-bottom: 1px solid #eeeeee; 491} 492code.sourcecode div:before { 493 display: inline-block; 494 content: counter(source-line); 495 counter-increment: source-line; 496 width: 4em; 497 color: #888888; 498 text-align: right; 499 margin-right: 20px; 500} 501code.sourcecode div.breakpoint:before { 502 margin-right: 0px; 503 border-right: 20px solid #ff0000; 504} 505code.sourcecode div.highlight { 506 background: #aaaaaa; 507 color: #000000; 508} 509code.sourcecode div.execution { 510 background: #000000; 511 color: #ffffff; 512} 513 514#source-select { 515 margin-top: 5px; 516} 517