body { font-family : Courier; }
.keyword { color: rgb(0,0,128); font-weight: bold;}
.identifier { color: rgb(102,14,122); }
.string_literal { color: green; }
.number { color: rgb(0,0,255); }
.comment { color: gray; }