div.source {
	font-family: courier, monospace;
	width:100%;
}

div.source p {
	margin:0px auto;
	line-height:1.2em;
	background-color:mintcream;
}

div.source p.alt {
	background-color:lavender;
}

code {
	font-family:courier, monosapce;
}

code.filename {
	font-weight:bold;
}

code.keyword {
	color:darkblue;
}

code.register {
	color:chocolate;
}

code.symbol {
	color:darkred;
}

code.inline {
	color:forestgreen;
}