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

.Editor .CodeMirror {
  height: 100%;
  font-size: 12px;
  line-height: 1.3;
  color: #999;
  background: #FFF;
}

.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 .node_def {
  color: black;
}
.Editor .node_ref {
  color: black;
  font-style: italic;
}
.Editor .comment {
  color: #509050;
  font-style: italic;
}