<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">/*
 *   style.css
 */

body {
     	margin: 5px;
	padding: 0px;
/*	color: #000; */
	color: #103020;
/*	background-color: #d0fff0;   */
/*	background-color: #e0fff0;   */
	background-color: #eaf0f0;  
}

a:link    {color: #7f7fff}
a:visited {color: #ff7f7f} 
a:active  {color: #ff0000}
a:hover   {color: #0000ff}

h1 {
   margin-left: 2pt;
   margin-right: 5pt;
   padding: 5pt;
   border-style: solid;
/*   border-width: 1pt 3pt 3pt 1pt; */
/* up,right,down,left */
   border-width: 1pt 1pt 1pt 8pt;
   border-color: #7070ff;
/*   background-color: #cfffdf;     */
   color: #000000;
   background-color: #c0c0ff; 
   clear: both;
}

h2 {
   margin-left: 0pt;
   margin-right: 5pt;
   padding: 5pt;
   border-style: solid;
   border-width: 1pt 1pt 1pt 5pt;
   border-color: #7070ff;
   color: #000000;
   background-color: #c0c0ff; 
   clear: both;
}

h3 {
   margin-left: 0pt;
   margin-right: 5pt;
   padding: 5pt;
   border-style: solid;
   border-width: 1pt 1pt 1pt 3pt;
   border-color: #7070ff;
   color: #000000;
   background-color: #c0c0ff; 
   clear: both;
}

span.sup { 
	 font-size: 60%;
	 vertical-align: 100%;
}

span.lineno {
	    color: #0000ff;
}

span.xline {
	    color: #ff0000;
}

span.emphasize {
	color: #ff0050;      
}

span.em {
	font-weight: bold;      
}

span.it {
	font-weight: italic;      
}

span.input { 
	color: #ff2750;
}

span.opt { 
	color: #0000ff;
}

span.ul {
	text-decoration: underline;	
}

span.footnote { 
	 font-size: 50%;
}

span.comment {
	color: #a020f0;      
}

/* main */
div.main {
	margin-left: 10px;
	margin-right: 10px;
	padding: 0px;
}

div.main hr {
	color: #a11;
	background-color: transparent;
}

div.main p {
	margin-top: 1em;
	margin-bottom: 1em;
	line-height: 120%;
}

div.main div.shell {
	color: #00007f;
	background-color:#f8f8ff;
	border-color: 	#aaaaaa;
	border-style: 	solid;
	border-width: 1px;
	margin: 0.5em 1em 0.5em 1em;
        padding: 20px;
        width: 90%;
}

div.main div.minibuff {
	color: #000000;
	background-color: #faebd7;
	border-color: 	#aaaaaa;
	border-style: 	solid;
	border-width: 1px;
	margin: 0.5em 1em 0.5em 1em;
/*
        margin-left: 2em;
        margin-right: 2em;
        margin-top: 0.7em;
        margin-bottom: 0.7em;
*/
        padding: 5px; 
        width: 90%;
}

div.main div.editor {
	color: #000000;
	background-color: #faebd7;
/*	clear: both;		   */
/*        border-style: dashed; */
	border-color: 	#aaaaaa;
	border-style: 	solid;
	border-width: 1px;
	margin: 0.5em 1em 0.5em 1em;
/*
        margin-left: 2em;
        margin-right: 2em;
        margin-top: 0.7em;
        margin-bottom: 0.7em;
*/
        width: 90%;
        padding: 5px; 
}

div.main div.code {
	color: 	black;
	font-style:	normal;
	font-weight:	normal;
	padding: 	20px;
/*	background-color: #faebd7; */
	background-color: white; 
	border-color: 	#aaaaaa;
	border-style: 	solid;
	border-width: 1px;
	margin: 0.5em 1em 0.5em 1em;
/*
	margin-left:	2em;
	margin-right:	2em;
        margin-top: 0.7em;
        margin-bottom: 0.7em;
*/
        width: 90%;
	clear: both;
}

div.main div.logsmall {
	width: 90%;
	border-style: dashed;
	border-width: 1px;
/*	border-color: #a11; */
	margin-top: 2em;
	margin-bottom: 2em;
	margin-left: 2em;
	padding: 4px;
	font-size: 60%;
}

div.main div.q {
	color: #000000;
	background-color: #efefe0;
	border-color: 	#aaaaaa;
	border-style: 	solid;
	border-width: 1px;
	margin: 1em 0.7em 0.7em 0.7em;
        padding: 10px; 
/*        width: 90%; */
}

div.main div.left {
	margin: 0.5em 1.0em 0.7em 0.7em;
	float: left;
}

div.main dt {
	 font-weight: bold;      
}

div.main pre {
	 clear: both;
}

div.main pre.src {
  background-color: #e0ffe0;  
  margin: 0.5em 1em 0.5em 1em;
  padding: 0.25em 0.5em 0.25em 0.5em;
  border-width: 1px;
  border-style: solid;
  border-color: #9fd0a0;
}

div.main pre.src2 {
  background-color: #c0ffc0;  
  margin: 0.5em 1em 0.5em 1em;
  padding: 0.25em 0.5em 0.25em 0.5em;
  border-width: 1px;
  border-style: solid;
  border-color: #8fd090;
}

div.main pre.shell {
	color: #00007f;
	background-color:#f8f8ff;
	border-color: 	#aaaaaa;
	border-style: 	solid;
	border-width: 1px;
	margin: 0.5em 1em 0.5em 1em;
        padding: 20px;
        width: 90%;
}

div.main pre.editor {
  background-color: #faebd7;
  margin: 0.5em 1em 0.5em 1em;
  padding: 0.25em 0.5em 0.25em 0.5em;
  border-width: 1px;
  border-style: solid;
  border-color: #aaaaaa;
}

div.dtree {
	font-size: 50%;
	text-decoration: none;
	text-align: left;
	margin-left: 5px;
	padding: 0px;
}

div.footer {
	font-size: 90%;
	text-decoration: none;
	text-align: right;
	margin-right: 1em;
	clear: both;
}

img.left {
	 clear: both;
	 float: left;
}

img {
    margin: 8px
}

img.inline {
    margin: 0px
}


p.clear {
	clear: both;
}</pre></body></html>