editor.css

body {
  margin-top: 25px;
  margin-left: 75px;
  margin-right: 75px;
}

caption {
    caption-side: top;
    font-weight: bold;
}

.hidden {
    display: none;
}

button:disabled {
    display: none;
    cursor: not-allowed;
    pointer-events: all !important;
}

.fetch-msg {
    font-weight: bold;
}

.CodeMirror {
    border: 2px solid;
    border-color: #C0C0C0; /*#F5F5F5;*/
    border-radius: 8px;
    margin-top: 1em;
    margin-bottom: 1em;
}

.preformatted {
    font-family: monospace;
    white-space: pre-wrap;
    font-size: 75%;
}

.line-error {
    background: #FBC2C4 !important;
    color: #8a1f11 !important;
}

#status-area {
    padding-top: 1em;
}

h1 {
    margin-top: 0.5em;
}