<style type=text/css>
//<link rel="stylesheet" type="text/css" href="./style.css">
.bug	{ color:black; }
.out	{
	color:#0000AA;
	background-color:#DDFFDD;
	border:solid 1px #AAAAAA;
	padding:0px 3px;
	font-family:monospace;
	white-space:pre;
	}
.lit	{
	color:#006600;
	background-color:#FFFFDD;
	border:solid 1px #AAAAAA;
	padding:0px 3px;
	font-family:monospace;
	font-weight:bold;
	white-space:pre;
	}
.lit0	{
	color:#006600;
	font-family:monospace;
	font-weight:bold;
	white-space:pre;
	}
.file,.filename	
	{
	color:#009999;
	font-family:sans-serif;
	font-weight:bold;
	white-space:pre;
	}
.name	
	{
	color:#0000AA;
	font-family:sans-serif;
	font-weight:bold;
	white-space:pre;
	}
.term	
	{
	color:#00AA00;
	font-family:sans-serif;
	font-style:italic;
	}
.var	{
	font-family:monospace; 
	color: darkred;
	}
.serr	{
	color: green;
	}
.taller	{
	line-height:140%;
	}
</style>
