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