devi@0: .cline,.wrong_cline,.interrupted_cline,.output,.wrong_output,.interrupted_output,.tab_cline, ._root_cline,.wrong_root_cline,.interrupted_root_cline,._root_output,.wrong_root_output,.interrupted_root_output,.tab_root_cline
devi@0: 		{ 
devi@0:         		margin		: 0px 0px 0px 0px;
devi@0:         		padding		: 0px 0px 0px 10px; 
devi@0: 			vertical-align	: top;
devi@0: 								}
devi@0: .cline,.wrong_cline,.interrupted_cline,.tab_cline,._root_cline,.wrong_root_cline,.interrupted_root_cline,.tab_root_cline
devi@0: 		{ 	font-weight	: bold;			}
devi@0: .wrong_output,.wrong_root_output	
devi@0: 		{ 	color		: #cc6666;		}
devi@0: .interrupted_output,.interrupted_root_output
devi@0: 		{ 	color		: #aaaaaa;		}
devi@0: .wrong_cline, .wrong_root_cline	
devi@0: 		{ 	color		: #ee7777; 		}
devi@0: .interrupted_cline, .interrupted_root_cline
devi@0: 		{ 	color		: #777777; 		}
devi@0: 
devi@0: ._root_cline,.wrong_root_cline,.interrupted_root_cline,._root_output,.wrong_root_output,.interrupted_root_output,.tab_root_cline
devi@0: 		{
devi@0: 			border-left	: #ff0000 solid thin;
devi@0: 			
devi@0: 		}
devi@0: 
devi@0: .note 		{ 
devi@0: 	color		: black;
devi@0: 	background 	: #d8fcff; 
devi@0:         margin		: 12px 12px 12px 12px;
devi@0:         padding		: 6px 6px 6px 6px; 
devi@0:         border-style	: dashed;
devi@0:         border-width	: thin;
devi@0: 	border-color 	: #a8eaff; 
devi@0: 	vertical-align	: top;
devi@0: }
devi@0: 
devi@0: .note_title,.note_text,.note_search	
devi@0: 		{ 
devi@0: 			color		: black;
devi@0:         		margin		: 0px 0px 0px 0px;
devi@0:         		padding		: 0px 0px 0px 0px; 
devi@0: 			vertical-align	: top;
devi@0: 								}
devi@0: .note_title	{ 	font-family	: sans-serif; 		}
devi@0: .note_text 	{ 	font-size	: 80%;			}
devi@0: .note_search 	{ 	text-align	: right; 		}
devi@0: 
devi@0: 
devi@0: .diff 		{ 
devi@0: 	color		: black;
devi@0: 	background 	: #fdffcd;
devi@0:         margin		: 16px 16px 16px 16px;
devi@0:         padding		: 6px 6px 6px 6px; 
devi@0:         border-style	: dashed;
devi@0:         border-width	: thin;
devi@0: }
devi@0: 
devi@0: .ttychange 		{ 
devi@0: 	color		: #9a9a9a;
devi@0: 	background 	: #e7e7e7;
devi@0:         margin		: 0px 0px 0px 0px;
devi@0:         padding		: 0px 0px 0px 0px; 
devi@0: 	vertical-align	: top;
devi@0: 	font-family	: monospace;
devi@0: }
devi@0: 
devi@0: .time 		{ 
devi@0: 	color		: #999999;
devi@0:         margin		: 0px 0px 0px 0px;
devi@0:         padding		: 0px 10px 0px 0px; 
devi@0: 	vertical-align	: top;
devi@0: 	font-size	: 80%;
devi@0: 	vertical-align	: top;
devi@0:  /*       border-right	: #9a9a9a solid thin; */
devi@0: }
devi@0: 
devi@0: .script 		{ 
devi@0:         margin		: 0px 0px 0px 0px;
devi@0:         padding		: 0px 0px 0px 0px; 
devi@0: 	vertical-align	: top;
devi@0: }
devi@0: 
devi@0: .visibility_form 		{ 
devi@0: 	color		: #9a9a9a;
devi@0: 	background 	: #e7e7e7;
devi@0:         margin		: 0px 0px 0px 0px;
devi@0:         padding		: 0px 0px 0px 0px; 
devi@0: 	vertical-align	: top;
devi@0: 	font-size	: 80%;
devi@0: 	font-family	: sans-serif;
devi@0: }