static-old/gcc.css

body {
    padding-top: 58px;
    padding-bottom: 40px;
}

/* Override the cursor that Bootstrap defines for readonly inputs, as it looks
 * very odd on IE (and 'text' makes it clearer that it's copyable everywhere).
 */
#permalink {
    cursor: text;
    width: 100%;
}

.btn.active {
    color: #fff;
    border-color: #46b8da;
    background-color: #5bc0de;
}

.autocompile {
    font-size: 18px;
    height: 24px;
    padding-top: 0;
}

#changetip_tipme_button {
    width: 80px;
}

#flattr_button {
    width: 120px;
}

.output {
    height: 80px;
    overflow: auto;
    font-family: monospace;
}

.compilers-container {
}

.compiler-options {
    margin-left: 10px; // space between the scroll-down and the compiler's options
    width: 100%;
}

.options {
    background: #ddf;
    border-radius: 4px;
    padding: 8px;
}

.options label {
    display: inline-block;
}

.inline-msg {
    font-family: arial;
    font-size: 70%;
    padding: 2px 5px 3px;
}

span.icon {
    border-radius: 50%;
    padding: 0 3px;
    margin-right: 7px;
}

.error {
    background: #faa !important;
    color: #a00;
}

.error span.icon {
    color: white;
    background-color: red;
    font-weight: bold;
}

.warning {
    background: #ffa !important;
    color: #440;
}

.warning span.icon {
    color: black;
    background-color: yellow;
}

.note {
    background: #aaf !important;
    color: #00a;
}

.note span.icon {
    color: white;
    background-color: blue;
}

.template {
    display: none;
}

li.social {
    padding: 4px;
}

.topbar {
    margin-top: 10px;
    padding: 6px;
    background: #eee;
    border-top-right-radius: 10px;
    border-top-left-radius: 10px;
}

.indented {
    margin-left: 36px;
}

/* These colours from Cynthia Brewer's excellent page at
 * http://colorbrewer2.org/
 */
.rainbow-0 {
    background: rgb(141, 211, 199) !important;
}

.rainbow-1 {
    background: rgb(255, 255, 179) !important;
}

.rainbow-2 {
    background: rgb(190, 186, 218) !important;
}

.rainbow-3 {
    background: rgb(251, 128, 114) !important;
}

.rainbow-4 {
    background: rgb(128, 177, 211) !important;
}

.rainbow-5 {
    background: rgb(253, 180, 98) !important;
}

.rainbow-6 {
    background: rgb(179, 222, 105) !important;
}

.rainbow-7 {
    background: rgb(252, 205, 229) !important;
}

.rainbow-8 {
    background: rgb(217, 217, 217) !important;
}

.rainbow-9 {
    background: rgb(188, 128, 189) !important;
}

.rainbow-10 {
    background: rgb(204, 234, 197) !important;
}

.rainbow-11 {
    background: rgb(255, 237, 111) !important;
}

.address {
    width: 4em;
    font-size: smaller;
}

.opcodes {
    width: 7em;
    overflow: hidden;
    font-size: smaller;
}

.opcode {
    color: #066;
    margin-right: 0.2em;
}

.opcode:nth-child(odd) {
    color: #060;
}

.highlighted {
    background-color: rgba(255, 0, 0, 0.2);
    color: #0000b0;
    font-weight: bold;
}


/* Only one of these class is currently used on index.html but just in case
 * we change it, it is already tuned */
.col-lg-1, .col-lg-10, .col-lg-11, .col-lg-12, .col-lg-2, .col-lg-3, .col-lg-4,
.col-lg-5, .col-lg-6, .col-lg-7, .col-lg-8, .col-lg-9, .col-md-1, .col-md-10,
.col-md-11, .col-md-12, .col-md-2, .col-md-3, .col-md-4, .col-md-5, .col-md-6,
.col-md-7, .col-md-8, .col-md-9, .col-sm-1, .col-sm-10, .col-sm-11, .col-sm-12,
.col-sm-2, .col-sm-3, .col-sm-4, .col-sm-5, .col-sm-6, .col-sm-7, .col-sm-8,
.col-sm-9, .col-xs-1, .col-xs-10, .col-xs-11, .col-xs-12, .col-xs-2, .col-xs-3,
.col-xs-4, .col-xs-5, .col-xs-6, .col-xs-7, .col-xs-8, .col-xs-9 {
    position: relative;
    min-height: 1px;
    padding-right: 0;
    padding-left: 0;
}

.panel-primary {
        border-color: #000;
}

.panel-body {
    padding-top: 15px;
    padding-right: 5px;
    padding-bottom: 5px;
    padding-left: 5px;
}

/* show the move cursor as the user moves the mouse over the panel header.*/
#draggablePanelList .panel-heading {
    cursor: move;
}

.panel-modest,
.panel-modest .panel-body {
      display: inline-block;
  }

.unselectable{
    /* disable text selection on character icons
     * source : http://stackoverflow.com/a/9314458/4669135 */
    -webkit-touch-callout: none;
    -webkit-user-select: none;
    -khtml-user-select: none;
    -moz-user-select: none;
    -ms-user-select: none;
    user-select: none;
}

.characterIcon {
    /* Show classical cursor when hovering */
    cursor: pointer;
}

.selectedCharacterIcon {
    color: #01DF01;
    font-size: 25px;
    margin-top: 0.4em;
    margin-right: 0.2em;
}

.unselectedCharacterIcon {
    color: #BDBDBD;
    font-size: 25px;
    margin-top: 0.4em;
    margin-right: 0.2em;
}

.unicode-arrow {
    font-size: 25px;
}

.unicodeCross {
    overflow: visible;
    font-weight: bold;
    color: #B90000;
    font-size: 20px; /* problem : it makes the panel header (title zone) bigger*/
    float: right;
}


.diff-before-button {
    background-color: rgba(251,175,175,.7);
}

.diff-after-button {
    background-color: rgba(151,234,151,.6);
}