/* Make the text editor has a nice style */
window.demo .view {
  color: #2e3436;
  font-family: Monospace;
  background-color: alpha(white, 0.30);
}

window.demo .view:selected {
  color: white;
  background-color: #4a90d9;
}

window.demo scrollbar trough,
.scrollbars-junction {
  background-color: alpha(white, 0.80);
}

window.demo scrollbar slider {
  border-width: 3px;
  border-style: solid;
  border-radius: 10px;
  border-color: transparent;
  background-clip: padding-box;
  background-color: #999;
}

window.demo scrollbar slider:hover {
  background-color: #555;
}

window.demo paned separator {
  background-color: alpha(white, 0.80);
  background-image: linear-gradient(transparent, transparent 1px, #999 1px, #999 4px, transparent 4px);
  background-size: 40px auto;
  background-repeat: no-repeat;
  background-position: center;
}

window.demo paned separator:hover {
  background-image: linear-gradient(transparent, transparent 1px, #555 1px, #555 4px, transparent 4px);
}