.highlight {
  border: 3px solid #7f9fbf;
  padding: 5px;
  margin: 3mm 0;
  margin-right: 2mm;
  display: inline-block;
}
code {
  border: 3px solid #7f9fbf;
  padding: 5px;
  margin: 3mm 0;
  margin-right: 2mm;
  display: inline-block;
  white-space: pre-wrap;
}
code span, .highlight span {
  white-space: inherit
}
dfn { color: blue; font-style: normal;}
.COMMENT1 {
	color: rgb(111,111,111);
}
.COMMENT2 {
	color: rgb(111,111,111);
	font-style: italic;
}
.COMMENT3 {
	color: rgb(99,99,99);
	background-color: rgb(247,247,247);
	font-style: italic;
}
.COMMENT4 {
	color: rgb(111,111,111);
	font-weight: bold;
}

.DIGIT {
	color: rgb(0,44,255);
}
.FUNCTION {
 	color: rgb(0,44,255);
 }
.INVALID {
	color: rgb(193,0,0);
 	font-weight: bold;
}

.KEYWORD1 {
	color: rgb(0,44,255);
	font-weight: bold;
}
.KEYWORD2 {
	color: #7f0055;
	font-weight: bold;
}
.KEYWORD3 {
	color: rgb(6,125,23);
	font-weight: bold;
}
.KEYWORD4 {
	color: #9E880D;
	font-weight: bold;
}
.LABEL {
	color: rgb(0,0,0);
	font-style: italic;
}

.LITERAL1 {
	color: rgb(6,125,23);
}
.LITERAL2 {
	color: #7f0055;
	font-weight: bold;
}
.LITERAL3 {
	color: rgb(0,44,255);
}
.LITERAL4 {
 	color: rgb(0,44,255);
}

.MARKUP {
	color: rgb(0,44,255);
}
.OPERATOR {
	color: rgb(0,0,0);
	font-weight: bold;
}