devi@90: h1,h2,h3,h4 {
devi@90:     color:  #485c9f;
devi@90:     padding-top:    10pt;
devi@90:     padding-bottom: 0pt;
devi@103:     margin-left:    0pt;
devi@90:     font-family:    sans-serif;
devi@90:     /*    border: thin solid gray; */
devi@90: }
devi@90: 
devi@90: a {
devi@90:     padding-left: 3pt;
devi@90:     padding-right: 3pt;
devi@90:     text-decoration: none;
devi@90: }
devi@90: 
devi@90: a:hover {
devi@90:     background-color: #eeeecc;
devi@90: }
devi@90: 
devi@90: body {
devi@90:     padding-left:   10pt;
devi@90:     font-family:    sans-serif;
devi@90: }
devi@90: 
devi@90: tr.table_header {
devi@90:     background-color    :   #98bcef;
devi@90:     font-weight:    bold;
devi@90:     font-size: 105%;
devi@90: }
devi@90: 
devi@90: td
devi@90: {
devi@90:     padding-left:5pt;
devi@90:     padding-right:5pt;
devi@90: 
devi@90:     margin-left:0pt;
devi@90:     margin-right:0pt;
devi@90: }
devi@90: 
devi@90: .toc {
devi@90:     border: 1px solid #aaa;
devi@90:     background-color: #f9f9f9;
devi@90:     padding: 10pt;
devi@90:     padding-left: 0pt;
devi@90:     padding-right: 15pt;
devi@90:     font-size: 95%;
devi@90: }
devi@90: 
devi@90: .files_toc {
devi@90:     padding : 10pt;
devi@90:     columns: 50em;
devi@90: }
devi@90: .toc_title {
devi@90:     font-weight: bold;
devi@90:     text-align: center;
devi@90: }
devi@90: 
devi@90: .cline, .output
devi@90:         { 
devi@90:     margin      : 0px 0px 0px 0em;
devi@90:     padding     : 0px 0px 0px 0px; 
devi@90:     vertical-align  : top;
devi@90:     /*display:inline;*/
devi@90: }
devi@90: 
devi@90: .cline
devi@90: {   font-weight : bold;           }
devi@90: 
devi@90: .wrong_cline, .wrong_root_cline,
devi@90: .mistyped_cline, .mistyped_root_cline   
devi@90:         {   
devi@90:             /*
devi@90:             color       : #ee7777;      
devi@90:             */
devi@90:             /* color        : #aa5555; */
devi@90:         }
devi@90: .wrong_output,              .wrong_root_output, 
devi@90: .mistyped_output,           .mistyped_root_output   
devi@90:         {   
devi@90:             /*
devi@90:             font-size   : 80%;
devi@90:             color       : #cc6666;      
devi@90:             */
devi@90:         }
devi@90: 
devi@90: .cblock_mistyped,
devi@90: .cblock_mistyped_root
devi@90:         {   
devi@90:             text-decoration : line-through;
devi@90:         }
devi@90: 
devi@90: .cblock_interrupted > .output,
devi@90: .cblock_interrupted_root > .output 
devi@90:         {
devi@90:             color       : #aaaaaa;
devi@90:         }
devi@90: 
devi@90: .cblock_interrupted > .cline
devi@90: .cblock_interrupted_root > .cline
devi@90:         {
devi@90:             color       : #777777;
devi@90:         }
devi@90: 
devi@90: 
devi@90: .cblock_normal_root,
devi@90: .cblock_wrong_root,
devi@90: .cblock_mistyped_root,
devi@90: .cblock_interrupted_root,
devi@90: .cblock_tab_root
devi@90:         {
devi@90:             border-left : #ff0000 solid thin;
devi@90:         }
devi@90: 
devi@90: .command    {
devi@90:     margin  : 0pt 0pt 0pt 0pt;
devi@90:     padding : 0pt 0pt 0pt 0pt;
devi@90:     /*border  : thin solid gray;*/
devi@90:         }
devi@90: 
devi@90: .with_hint  {
devi@90:     background  :   #effdff;
devi@90: }
devi@90: 
devi@90: .without_hint   {
devi@90:     background  :   #ffefef;
devi@90: }
devi@90: 
devi@90: .note       { 
devi@90:     /*     
devi@90:     color       : black;
devi@90:     background  : #d8fcff; 
devi@90:     margin      : 12px 12px 12px 12px;
devi@90:         padding     : 6px 6px 6px 6px; 
devi@90:         border-style    : dashed;
devi@90:         border-width    : thin;
devi@90:     border-color    : #a8eaff; 
devi@90:     vertical-align  : top;
devi@90:     */
devi@90:     color       : black;
devi@90:     background  : #d8f0ff;
devi@90:     margin      : 2px 12px 12px 12px;
devi@90:         padding     : 6px 6px 6px 6px; 
devi@90:         border-style    : dotted;
devi@90:         border-width    : thin;
devi@90:     border-color    : #687cbf;
devi@90:     vertical-align  : top;
devi@90: }
devi@90: 
devi@90: .note_title,.note_text,.note_search 
devi@90:         { 
devi@90:             color       : black;
devi@90:                 margin      : 0px 0px 0px 0px;
devi@90:                 padding     : 0px 0px 0px 0px; 
devi@90:             vertical-align  : top;
devi@90:                                 }
devi@90: .note_title {   
devi@90:             font-size   : 120%;         
devi@90:             font-family : sans-serif;
devi@90:             padding-top : 2pt;
devi@90:             padding-bottom  : 2pt;
devi@90:         }
devi@90: .note_text  {   
devi@90:             font-family : sans-serif;       
devi@90:             font-size   : 100%;         
devi@90:         }
devi@90: .note_search    {   text-align  : right;        }
devi@90: 
devi@90: 
devi@90: .diff       { 
devi@90:     color       : black;
devi@90:     background  : #fdffcd;
devi@90:         margin      : 16px 16px 16px 16px;
devi@90:         padding     : 6px 6px 6px 6px; 
devi@90:         border-style    : dashed;
devi@90:         border-width    : thin;
devi@90: }
devi@90: 
devi@90: .ttychange      { 
devi@90:     color       : #9a9a9a;
devi@90:     background  : #fafafa;
devi@90:     margin      : 0em 0px 0pt 0px;
devi@90:     padding     : 0em 0pt 0em 0pt; 
devi@90:     vertical-align  : top;
devi@90:     font-family : monospace;
devi@90:     min-width: 5em;
devi@90:     position    : relative;
devi@90:     left        : 0em;
devi@90:     border-top  : thin dotted #cccccc;
devi@90:     text-align  : right;
devi@90:     font-size   : 50%;
devi@90: }
devi@90: 
devi@90: .time { 
devi@90:     color       : #999999;
devi@90:     margin      : 0px 0px 0px 0px;
devi@90:     padding     : 2pt 5pt 0px 0px; 
devi@90:     vertical-align  : top;
devi@90:     font-size   : 80%;
devi@90:     width       : 5em;
devi@90:     float       : left; 
devi@90: /*    height      : 100%; */
devi@90: /*    border      : thin solid gray; */
devi@90: }
devi@90: 
devi@90: .cblock,
devi@90: .cblock_normal,
devi@90: .cblock_wrong,
devi@90: .cblock_mistyped,
devi@90: .cblock_interrupted,
devi@90: .cblock_tab,
devi@90: .cblock_normal_root,
devi@90: .cblock_wrong_root,
devi@90: .cblock_mistyped_root,
devi@90: .cblock_interrupted_root,
devi@90: .cblock_tab_root
devi@90: { 
devi@90:     margin      : 0px 0px 0px 0em;
devi@90:     padding     : 0px 0px 0px 5pt; 
devi@90:     vertical-align  : top;
devi@90: /*    border      : thin solid blue; */
devi@90: }
devi@90: 
devi@90: .visibility_form        { 
devi@90:     position    : fixed;
devi@90:     bottom: 10; right: 10;
devi@90:     z-index     : 5;
devi@90:     color       : #9a9a9a;
devi@90:     background  : #e7e7e7;
devi@90:     margin      : 0px 0px 0px 0px;
devi@90:     padding     : 0px 0px 0px 0px; 
devi@90:     vertical-align  : top;
devi@90:     font-size   : 80%;
devi@90:     font-family : sans-serif;
devi@90: }
devi@90: .visibility_form > .header {
devi@90:     font-weight: bold;
devi@90: }
devi@90: .visibility_form > .window_controls {
devi@90:     position : absolute;
devi@90:     right : 1pt;
devi@90: }
devi@90: 
devi@90: .new_commands_table {
devi@90:         padding     : 0px 0px 0px 0px;
devi@90:         margin      : 20px 60px 60px 20px;
devi@90:         background-color: #f9f9f9;
devi@90: }
devi@90: 
devi@90: .new_commands_header {
devi@90:         font-weight: bold;
devi@90:         background-color: #e9e9e9;
devi@90: }
devi@90: 
devi@90: .new_commands_caption {
devi@90:         font-style: italic;
devi@90:         background-color: #ffffff;
devi@90: }
devi@90: 
devi@90: .err_box {
devi@90:     color       : white;
devi@90:     background  : red;
devi@90:     font-weight : bold;
devi@90:     font-size   : 70%;
devi@90: }
devi@90: .filename, .file_navigation {
devi@90:     background  : #f7f7ba;
devi@90:     padding     : 1ex;
devi@90:     padding-bottom: 1pt;
devi@90:     display     : inline;
devi@90: }
devi@90: 
devi@90: .filename {
devi@90:     font-weight : bold;
devi@90:     margin      :  20pt 0pt 0pt 10pt;
devi@90: }
devi@90: 
devi@90: .file_navigation {
devi@90:     font-weight : bold;
devi@90:     margin      :  20pt 10pt 0pt 0pt;
devi@90: }
devi@90: 
devi@90: .filedata {
devi@90:     padding: 5pt 10pt 5pt 10pt;
devi@90:     margin:  0pt 10pt 30pt 10pt;
devi@90:     border-left: 2pt;
devi@90:     border-right: 2pt;
devi@90:     border-bottom: 2pt;
devi@90:     border-style: solid;
devi@90:     border-color: #f7f7ba;
devi@90:     background-color: #fffffa;
devi@90: }
devi@90: 
devi@90: .time_passed {
devi@90:     padding: 1em 5em 1em 5em
devi@90: }
devi@90: 
devi@90: .much_time_passed {
devi@90:     padding: 2em 5em 2em 5em
devi@90: }
devi@90: 
devi@90: .edit_link {
devi@90:     float:      right;
devi@90:     font-size:  80%;
devi@90:     position: relative;
devi@90:     bottom: 0;
devi@90:     padding-top: 2em;
devi@90: }
devi@90: 
devi@90: .lined_header {
devi@90:     border-bottom: 1pt solid gray;
devi@90:     padding: 10pt 0pt 5pt 0pt;
devi@90:     margin: 30pt 0pt 20pt 0pt;
devi@90: }
devi@90: 
devi@90: 
devi@101: .nav_bar {
devi@101:     font-size: 80%;
devi@101:     color: #222222;
devi@101:     background-color: #eeeeee;
devi@101: }
devi@90: 
devi@101: /*
devi@101: .nav_bar a {
devi@101:     color: #222222;
devi@101:     padding-left: 1pt;
devi@101:     padding-right: 1pt;
devi@101: }
devi@101: */
devi@101: body {
devi@101:     margin:0;
devi@101:     padding:0 0 15px 0;
devi@101: 
devi@101: }
devi@101: .body {
devi@101:     margin: 10;
devi@101:     padding: 10;
devi@101: }