.Editor .status_bar {
  height: 22px;
  background: #DDD;
  border-top: 1px solid gray;
  font-family: sans-serif;
  font-size: 12px;
  padding: 4px;
  box-sizing: border-box;
}
.Editor .error {
  background: #F77;
}

.Editor {
  display: flex;
  flex-direction: column;
}
.Editor .editor_div {
  flex-grow: 1;
  height: 0;
}

.Editor .CodeMirror {
  height: 100%;
  font-size: 12px;
  font-family: sans-serif;
  line-height: 1.3;
  background: #F7F7F7;
  margin-left: 4px;
  margin-right: 4px;
}
.Editor .CodeMirror-gutters {
  border-right: 0;
}
.Editor .CodeMirror-lines > * {
  border: 1px solid #DDD;
  background: white;
}

.Editor .span {
  background: rgba(255, 165, 0, 0.15);
}
.Editor .code {
  color: rgba(200, 76, 0, 0.8);
  font-weight: bold;
}
.Editor .error {
  background: rgba(255,0,0,0.2);
  border-bottom: 2px solid red;
}