1 body {

     2 	overflow: hidden;

     3 }

     4 

     5 h1 {

     6 	font-size: 14px;

     7 	margin: 0 0 10px 0;

     8 }

     9 

    10 h2 {

    11 	font-size: 12px;

    12 	margin: 3px 0 3px 0;

    13 }

    14 

    15 h3 {

    16 	font-size: 11px;

    17 	margin: 3px 0 3px 0;

    18 }

    19 

    20 #log {

    21 	font-family: Verdana;

    22 	border: 1px solid gray;

    23 	width: 100%; height: 240px;

    24 	overflow: scroll;

    25 	white-space: nowrap;

    26 }

    27 

    28 #log span {

    29 	display: block;

    30 }

    31 

    32 #log span.msg {

    33 	float: left;

    34 }

    35 

    36 #log span.time {

    37 	float: left;

    38 }

    39 

    40 #log br {

    41 	clear: both;

    42 }

    43 

    44 #logfilter {

    45 	width: 350px;

    46 }

    47 

    48 #logenabled {

    49 	border: 0;

    50 }

    51 

    52 #settings_panel span, #info_panel span, #content_panel span, #command_states_panel span, #undo_redo_panel span {

    53 	display: block;

    54 	margin: 5px 0 5px 0;

    55 }

    56 

    57 div.data {

    58 	width: 100%; height: 240px;

    59 	overflow: scroll;

    60 	border: 1px solid gray;

    61 }

    62 

    63 #misc_panel div.data {

    64 	height: 270px;

    65 }

    66 

    67 .data input {

    68 	width: 265px;

    69 	border: 0;

    70 }

    71 

    72 .data h2 {

    73 	margin-left: 5px;

    74 }

    75 

    76 .data h3 {

    77 	margin-left: 7px;

    78 }

    79 

    80 .data div {

    81 	margin-left: 7px;

    82 }

    83 

    84 .data table {

    85 	margin: 0 0 15px 15px;

    86 }

    87 

    88 .data p {

    89 	margin: 0; padding: 0;

    90 	margin-top: 5px;

    91 	margin-left: 5px;

    92 }

    93 

    94 table, td {

    95 	border: 1px solid gray;

    96 	border-collapse: collapse;

    97 }

    98 

    99 #flip {

   100 	position: absolute;

   101 	left: 295; top: 384px;

   102 }

   103 

   104 .bspec {

   105 	color: gray;

   106 }

   107 

   108 .dep {

   109 	color: #880000;

   110 }

   111 

   112 .col1 {

   113 	width: 265px;

   114 }

   115 

   116 div.undodata {

   117 }