+ margin: 0 0.5em;
+ border: 0;
+ width: 88px;
+ height: 32px; /* this should be 31px */
+}
+
+/* foreground colors (life cycle, grammar) **********************************/
+
+.delta {
+ color:#500000;
+}
+
+.gamma {
+ color:#006000;
+}
+
+.beta {
+ color:#906000;
+}
+
+.alpha {
+ color:#000000;
+}
+
+.ebnf {
+ color:#000080;
+}
+
+/* mark colors **************************************************************/
+
+.red-mark {
+ color:#F00000;
+}
+
+.green-mark {
+ color:#00F000;
+}
+
+.blue-mark {
+ color:#0000F0;