.hdevelop {
    color: rgb(0,0,150);
    font-weight: normal;
    background-color: rgb(250,250,250);
    white-space: pre;
    font-family: Consolas, monospace;
    display: inline-block;
    margin: 3px;
    padding: 6px 15px;
    border-style: solid;
    border-width: thin;
    border-color: #F28D26;
    border-top: 15px solid #F28D26;
  }
  
.hdev-operator {
    color: rgb(0,0,150);
}
.hdev-internal-ops { /* e.g. dev_display */
    color: rgb(100,70,20);
}
.hdev-internal-procs {
    color: rgb(100,0,150);
}
.hdev-external-procs {
    color: rgb(0,100,150);
}
.hdev-controlstatement {
    color: rgb(120,60,40);
}
.hdev-comment {
    color: rgb(0,150,0);
}