Annotation of modules/damieng/graphical_editor/daxe/lib/daxe.css, revision 1.2

1.1       damieng     1: body {
                      2:   line-height: 1.5;
                      3:   color: black;
                      4:   background-color: white;
                      5:   overflow: hidden;
                      6: }
                      7: 
                      8: button {
                      9:   padding: 2px;
                     10: }
                     11: 
                     12: #headers {
                     13:   position: absolute;
                     14:   top: 0em;
                     15:   left: 0em;
                     16:   right: 0em;
                     17:   z-index: 5;
                     18: }
                     19: 
                     20: #left_panel {
                     21:   position: absolute;
                     22:   top: 4em;
                     23:   bottom: 1.3em;
                     24:   left: 0em;
                     25:   width: 15em;
                     26:   z-index: 1;
                     27:   background-color: #F0F0F0;
                     28: }
                     29: 
                     30: #tab_buttons {
                     31:   position: absolute;
                     32:   top: 0em;
                     33:   left: 0em;
                     34:   right: 0em;
                     35:   border-bottom: 1px solid #555;
                     36:   background-color: #F5F5F5;
                     37:   z-index: 3;
                     38: }
                     39: 
                     40: .tab_button {
                     41:   position: relative;
                     42:   top: 1px;
                     43:   display: inline-block;
                     44:   vertical-align: bottom;
                     45:   border: 1px solid #555;
                     46:   padding-left: 4px;
                     47:   padding-right: 4px;
                     48:   padding-top: 2px;
                     49:   padding-bottom: 2px;
                     50:   background-color: #F5F5F5;
                     51:   border-top-left-radius: 0.4em;
                     52:   border-top-right-radius: 0.4em;
                     53:   cursor: default;
                     54:   -webkit-user-select: none;
                     55:   -khtml-user-select: none;
                     56:   -moz-user-select: none;
                     57:   -ms-user-select: none;
                     58:   user-select: none;
                     59: }
                     60: 
                     61: .tab_button:hover {
                     62:   background-color: #DDD;
                     63: }
                     64: 
                     65: .tab_button:focus {
                     66:   outline: none;
                     67:   box-shadow: inset 0px 0px 1px 1px #50A0FF;
                     68: }
                     69: 
                     70: .tab_button.selected {
                     71:   border-bottom: 1px solid #F0F0F0;
                     72:   background-color: #F0F0F0;
                     73:   color: black;
                     74: }
                     75: 
                     76: #insert {
                     77:   position: absolute;
                     78:   top: 2em;
                     79:   bottom: 0em;
                     80:   left: 0em;
                     81:   width: 15em;
                     82:   overflow: auto;
                     83:   text-align: center;
                     84:   background-color: #F0F0F0;
                     85: }
                     86: 
                     87: #tree {
                     88:   position: absolute;
                     89:   top: 2em;
                     90:   bottom: 0em;
                     91:   left: 0em;
                     92:   width: 15em;
                     93:   overflow: auto;
                     94:   background-color: #F0F0F0;
                     95:   white-space: pre;
                     96: }
                     97: 
                     98: .tree_div {
                     99:   position: relative;
                    100:   margin-left: 0.5em;
                    101: }
                    102: 
                    103: .expand_button {
                    104:   position: absolute;
                    105:   left: -14px;
                    106:   top: 0px;
                    107:   display: inline-block;
                    108:   padding-left: 1px;
                    109:   padding-right: 1px;
                    110:   margin-right: 2px;
                    111:   text-align: center;
                    112:   cursor: default;
                    113:   -webkit-user-select: none;
                    114:   -khtml-user-select: none;
                    115:   -moz-user-select: none;
                    116:   -ms-user-select: none;
                    117:   user-select: none;
                    118: }
                    119: 
                    120: .expand_button:hover {
                    121:   background-color: #DDD;
                    122: }
                    123: 
                    124: .tree_node_title {
                    125:   cursor: default;
                    126:   -webkit-user-select: none;
                    127:   -khtml-user-select: none;
                    128:   -moz-user-select: none;
                    129:   -ms-user-select: none;
                    130:   user-select: none;
                    131: }
                    132: 
                    133: .tree_node_title:focus {
                    134:   outline: none;
                    135:   box-shadow: 0px 0px 1px 1px #50A0FF;
                    136: }
                    137: 
                    138: .tree_node_title:hover {
                    139:   background-color: #DDD;
                    140: }
                    141: 
                    142: #insert button.insertb {
                    143:   width: 80%
                    144: }
                    145: 
                    146: 
                    147: div.menubar {
                    148:   background-color: #FFFFFF;
                    149:   color: #000;
                    150:   border-bottom: 1px solid #000;
                    151:   cursor: default;
                    152:   z-index: 10;
                    153:   -webkit-user-select: none;
                    154:   -khtml-user-select: none;
                    155:   -moz-user-select: none;
                    156:   -ms-user-select: none;
                    157:   user-select: none;
                    158:   font-family: sans-serif;
                    159: }
                    160: 
                    161: div.menu_title {
                    162:   position: relative;
                    163:   display: inline-block;
                    164:   padding-left: 0.5em;
                    165:   padding-right: 0.5em;
                    166:   font-size: 0.9rem;
                    167: }
                    168: 
                    169: .menu_title .disabled {
                    170:   color: #AAA;
                    171: }
                    172: 
                    173: .menu_title:focus {
                    174:   outline: none;
                    175:   box-shadow: inset 0px 0px 1px 1px #50A0FF;
                    176: }
                    177: 
                    178: div.dropdown_menu {
                    179:   position: absolute;
                    180:   left: 0px;
                    181:   top: 100%;
                    182:   min-width: 5em;
                    183:   white-space: nowrap;
                    184:   z-index: 10;
                    185:   font-family: sans-serif;
                    186:   font-size: 0.9rem;
                    187: }
                    188: 
                    189: table.menu {
                    190:   border-spacing: 0px;
                    191:   color: #000;
                    192:   background-color: #FFFFFF;
                    193:   border: 1px solid #000;
                    194:   box-shadow: 2px 2px 2px #AAA;
                    195: }
                    196: 
                    197: table.menu tr td {
                    198:   position: relative;
                    199:   padding-left: 5px;
                    200:   padding-right: 5px;
                    201:   cursor: default;
                    202: }
                    203: 
                    204: table.menu tr.checked td:nth-of-type(2)::after {
                    205:   content: "✓";
                    206: }
                    207: 
                    208: div.submenu {
                    209:   position: absolute;
                    210:   left: 100%;
                    211:   top: 0px;
                    212:   width: 20em;
                    213:   z-index: 10;
                    214: }
                    215: 
                    216: .disabled {
                    217:   color: #A0A0A0;
                    218: }
                    219: 
                    220: 
                    221: .toolbar {
                    222:   cursor: default;
                    223:   z-index: 5;
                    224:   padding: 1px;
                    225:   background: linear-gradient(#F5F5F5, #DADADA);
                    226:   box-shadow: 2px 2px 2px #AAA;
                    227:   -webkit-user-select: none;
                    228:   -khtml-user-select: none;
                    229:   -moz-user-select: none;
                    230:   -ms-user-select: none;
                    231:   user-select: none;
                    232: }
                    233: 
                    234: .toolbar-box {
                    235:   display: inline-block;
                    236:   line-height: 20px;
                    237:   border: 1px solid #AAA;
                    238:   margin: 0.2em;
                    239:   background: #FAFAFA;
                    240:   border-radius: 5px;
                    241:   overflow: hidden;
                    242:   vertical-align: top;
                    243: }
                    244: 
                    245: .toolbar-menu {
                    246:   display: inline-block;
                    247:   line-height: 20px;
                    248:   border: 1px solid #AAA;
                    249:   margin: 0.3em;
                    250:   background: #FFFFFF;
                    251:   vertical-align: top;
                    252: }
                    253: 
                    254: .toolbar-button {
                    255:   display: inline-block;
                    256:   line-height: 18px;
                    257:   padding: 3px;
                    258: }
                    259: 
                    260: .button-disabled {
                    261:   opacity: 0.3;
                    262: }
                    263: 
                    264: .button-selected {
                    265:   background-color: #CCC;
                    266: }
                    267: 
                    268: .toolbar-button:hover {
                    269:   background-color: #DDD;
                    270: }
                    271: 
                    272: .toolbar-button:focus {
                    273:   outline: none;
                    274:   box-shadow: inset 0px 0px 1px 1px #50A0FF;
                    275: }
                    276: 
                    277: .toolbar-button:focus img {
                    278: }
                    279: 
                    280: .toolbar-button.button-disabled:hover {
                    281:   background-color: transparent;
                    282: }
                    283: 
                    284: .toolbar-button img {
                    285:   vertical-align: middle;
                    286: }
                    287: 
                    288: div#doc1 {
                    289:   position: absolute;
                    290:   bottom: 1.3em;
                    291:   left: 15em;
                    292:   right: 0em;
                    293:   top: 4em;
                    294:   overflow: auto;
                    295: }
                    296: 
                    297: div#doc2 {
1.2     ! damieng   298:   height: 100%;
1.1       damieng   299:   cursor: text;
                    300:   padding-right: 3px;
                    301: }
                    302: 
                    303: div#path {
                    304:   position: fixed;
                    305:   left: 0px;
                    306:   bottom: 0px;
                    307:   width: 100%;
                    308:   height: 1.5em;
                    309:   z-index: 2;
                    310:   border-top: 1px solid #999;
                    311:   font-family: sans-serif;
                    312:   font-size: 85%;
                    313:   background-color: #F0F0F0;
                    314:   color: #000000;
                    315: }
                    316: 
                    317: textarea#tacursor {
                    318:   position: absolute;
                    319:   width: 0.5em;
                    320:   height: 1em;
                    321:   border: medium none;
                    322:   opacity: 0;
                    323:   resize: none;
                    324:   pointer-events: none;
                    325:   text-indent: -1em;
                    326: }
                    327: 
                    328: span#caret {
                    329:   position: absolute;
                    330:   width: 1em;
                    331:   height: 1em;
                    332:   border-left: 2px solid #555;
                    333:   pointer-events: none;
                    334:   cursor: text;
                    335:   z-index: 5;
                    336: }
                    337: 
                    338: span#caret.horizontal {
                    339:   border-top: 2px solid #555;
                    340:   border-left: none;
                    341: }
                    342: 
                    343: .dn {
                    344:   word-wrap: break-word;
                    345:   white-space: pre-wrap;
                    346: }
                    347: 
                    348: div.indent {
                    349:   margin-left: 1.5em;
                    350: }
                    351: 
                    352: /* Tag */
                    353: span.empty_tag, span.start_tag, span.end_tag, span.simple_type {
                    354:   font-family: sans-serif;
                    355:   font-weight: normal;
                    356:   font-style: normal;
                    357:   font-size: 85%;
                    358:   text-align: left;
                    359:   color: #000000;
                    360:   background-color: #FFFFB0;
                    361:   border: 1px solid #707070;
                    362:   margin-left: 2px;
                    363:   margin-right: 2px;
                    364:   padding-top: 1px;
                    365:   padding-bottom: 1px;
                    366:   -webkit-touch-callout: none;
                    367:   -webkit-user-select: none;
                    368:   -khtml-user-select: none;
                    369:   -moz-user-select: none;
                    370:   -ms-user-select: none;
                    371:   user-select: none;
                    372:   box-shadow: 1px 1px 1px #A0A0A0;
                    373:   cursor: default;
                    374: }
                    375: 
                    376: span.empty_tag {
                    377:   padding-left: 2px;
                    378:   padding-right: 2px;
                    379: }
                    380: 
                    381: span.start_tag {
                    382:   border-top-right-radius: 0.6em;
                    383:   border-bottom-right-radius: 0.6em;
                    384:   padding-left: 2px;
                    385:   padding-right: 0.5em;
                    386: }
                    387: 
                    388: span.end_tag {
                    389:   border-top-left-radius: 0.6em;
                    390:   border-bottom-left-radius: 0.6em;
                    391:   padding-left: 0.5em;
                    392:   padding-right: 2px;
                    393: }
                    394: 
                    395: .selected span.empty_tag, .selected span.start_tag, .selected span.end_tag, span.selected.simple_type,
                    396:     .selected span.simple_type {
                    397:   background-color: #F05030;
                    398:   color: #FFFFFF;
                    399: }
                    400: .invalid.selected>span.empty_tag, .invalid.selected>span.start_tag, .invalid.selected>span.end_tag,
                    401:     .selected .invalid>span.empty_tag, .selected .invalid>span.start_tag, .selected .invalid>span.end_tag {
                    402:   background-color: #F07030;
                    403: }
                    404: 
                    405: .selected {
                    406:   background-color: #50A0FF;
                    407:   color: #FFFFFF;
                    408: }
                    409: 
                    410: .invalid>span.empty_tag, .invalid>span.start_tag, .invalid>span.end_tag {
                    411:   background-color: #FFE0A0;
                    412: }
                    413: 
                    414: span.start_tag img, span.empty_tag img {
                    415:   vertical-align: middle;
                    416: }
                    417: span.start_tag img:hover, span.empty_tag img:hover {
                    418:   background-color: #F0F0B0;
                    419: }
                    420: .selected span.empty_tag img:hover, .selected span.start_tag img:hover,
                    421: .selected span.end_tag img:hover, span.selected.simple_type img:hover {
                    422:   background-color: #F07050;
                    423: }
                    424: 
                    425: span.long {
                    426:   display: inline-block;
                    427:   width: 90%;
                    428:   line-height: 1.2em;
                    429: }
                    430: 
                    431: span.attribute_name {
                    432:   color: #000090;
                    433: }
                    434: 
                    435: span.attribute_value {
                    436:   color: #005000;
                    437: }
                    438: 
                    439: /* dialogs */
                    440: div.dlg1 {
                    441:   position: absolute;
                    442:   left: 0px;
                    443:   top: 0px;
                    444:   width: 100%;
                    445:   height: 100%;
                    446:   z-index: 10;
                    447:   background-color:rgba(127, 127, 127, 0.5);
                    448: }
                    449: 
                    450: div.dlg2 {
                    451:   position: absolute;
                    452:   left: 50%;
                    453:   height: 100%;
                    454: }
                    455: 
                    456: div.dlg3 {
                    457:   position: relative;
                    458:   left: -50%;
                    459:   top: 1em;
                    460:   max-height: 90%;
                    461:   min-width: 250px;
                    462:   overflow: auto;
                    463:   padding: 1em;
                    464:   background-color: #FFFFFF;
                    465:   border: solid 1px #202020;
                    466:   box-shadow: 2px 2px 2px #A0A0A0;
                    467: }
                    468: 
                    469: div.dlgtitle {
                    470:   text-align: center;
                    471:   font-family: sans-serif;
                    472:   font-size: 120%;
                    473:   margin-bottom: 1em;
                    474: }
                    475: 
                    476: div.buttons {
                    477:   text-align: right;
                    478: }
                    479: 
                    480: div.buttons button {
                    481:   margin: 5px;
                    482: }
                    483: 
                    484: input.valid {
                    485:   color: #006000;
                    486: }
                    487: 
                    488: input.invalid {
                    489:   color: #F00000;
                    490: }
                    491: 
                    492: input:-webkit-autofill {
                    493:   -webkit-box-shadow: 0 0 0px 1000px white inset;
                    494:   -webkit-text-fill-color: #006000;
                    495: }
                    496: 
                    497: .required {
                    498:   color: #B00000;
                    499: }
                    500: 
                    501: .optional {
                    502:   color: #005000;
                    503: }
                    504: 
                    505: /* help */
                    506: button.help {
                    507:   line-height: 1em;
                    508:   font-size: 80%;
                    509:   padding: 2px;
                    510:   margin-right: 7px;
                    511: }
                    512: 
                    513: div.dlg3 table {
                    514:   border-spacing: 5px;
                    515: }
                    516: 
1.2     ! damieng   517: .help_element_name {
        !           518:   font-family: monospace;
        !           519: }
        !           520: 
        !           521: .help_attribute_name {
        !           522:   font-family: monospace;
        !           523: }
        !           524: 
        !           525: .help_default_value {
1.1       damieng   526:   font-family: monospace;
                    527: }
                    528: 
                    529: div.help_regexp {
                    530:   font-family: monospace;
                    531:   margin-bottom: 1em;
                    532:   word-break: break-all;
                    533: }
                    534: 
                    535: span.help_list_title {
                    536:   position: relative;
                    537:   margin-right: 2px;
                    538:   border-top: 1px solid #505050;
                    539:   border-left: 1px solid #505050;
                    540:   border-right: 1px solid #505050;
                    541:   padding-left: 4px;
                    542:   padding-right: 4px;
                    543:   padding-top: 2px;
                    544:   padding-bottom: 2px;
                    545:   background-color: #F0F0F0;
                    546:   border-top-left-radius: 0.4em;
                    547:   border-top-right-radius: 0.4em;
                    548:   cursor: default;
                    549: }
                    550: 
                    551: span.help_list_title.selected_tab {
                    552:   top: 3px;
                    553:   z-index: 3;
                    554: }
                    555: 
                    556: div.help_list_div {
                    557:   height: 15em;
                    558:   overflow: auto;
                    559:   border: 1px solid #505050;
                    560:   background-color: #F0F0F0;
                    561: }
                    562: 
                    563: ul#help_list {
                    564:   margin-top: 0px;
                    565: }
                    566: 
                    567: li.help_selectable:hover {
                    568:   cursor: default;
                    569:   color: #30A0F0;
                    570: }
                    571: 
                    572: /* find */
                    573: div.find {
                    574:   position: absolute;
                    575:   bottom: 1.5em;
                    576:   left: 15em;
                    577:   right: 0em;
                    578:   height: 9em;
                    579:   overflow: auto;
                    580:   background-color: #FFFFFF;
                    581:   color: #000000;
                    582:   border: 1px solid #505050;
                    583: }
                    584: 
                    585: div.options label {
                    586:   margin-right: 1em;
                    587: }
                    588: 
                    589: /* source */
                    590: div.source_window {
                    591:   position: absolute;
                    592:   z-index: 5;
                    593:   left: 1em;
                    594:   top: 2.5em;
                    595:   right: 1em;
                    596:   bottom: 1em;
                    597:   overflow: auto;
                    598:   background-color: #FFFFFF;
                    599:   border: solid 1px #202020;
                    600:   box-shadow: 2px 2px 2px #A0A0A0;
                    601: }
                    602: 
                    603: div.source_content {
                    604:   position: absolute;
                    605:   z-index: 10;
                    606:   left: 1em;
                    607:   top: 1em;
                    608:   right: 1em;
                    609:   bottom: 3em;
                    610:   overflow: auto;
                    611:   font-family: monospace;
                    612:   word-wrap: break-word;
                    613:   white-space: pre-wrap;
                    614:   background-color: #FFFFFF;
                    615:   border: solid 1px #A0A0A0;
                    616: }
                    617: 
                    618: div.source_bottom {
                    619:   position: absolute;
                    620:   z-index: 10;
                    621:   left: 1em;
                    622:   right: 1em;
                    623:   bottom: 0em;
                    624:   height: 2em;
                    625:   text-align: center;
                    626:   background-color: #FFFFFF;
                    627: }
                    628: 
                    629: span.source_element_name {
                    630:   color: #A00000;
                    631: }
                    632: 
                    633: span.source_attribute_name {
                    634:   color: #0000A0;
                    635: }
                    636: 
                    637: span.source_attribute_value {
                    638:   color: #006400;
                    639: }
                    640: 
                    641: span.source_entity {
                    642:   color: #006464;
                    643: }
                    644: 
                    645: span.source_comment {
                    646:   color: #505050;
                    647: }
                    648: 
                    649: span.source_cdata {
                    650:   color: #503000;
                    651: }
                    652: 
                    653: span.source_pi {
                    654:   color: #640064;
                    655: }
                    656: 
                    657: span.source_doctype {
                    658:   color: #646400;
                    659: }
                    660: 
                    661: /* selection */
                    662: .selection {
                    663:   background-color: #50A0FF;
                    664:   color: #FFFFFF;
                    665: }
                    666: 
                    667: /* DNAnchor */
                    668: .anchor {
                    669:   text-decoration: underline;
                    670:   color: #0000EE;
                    671: }
                    672: .anchor img {
                    673:   cursor: default;
                    674: }
                    675: 
                    676: /* DNHiddenP */
                    677: .hiddenp {
                    678:   position: relative;
                    679:   min-height: 1.5em;
                    680: }
                    681: .hiddenp::after {
                    682:   position: absolute;
                    683:   right: 1px;
                    684:   bottom: 1px;
                    685:   content: " ¶";
                    686:   color: #CCC;
                    687:   z-index: -1;
                    688: }
                    689: 
                    690: /* DNList */
                    691: ul.list {
                    692:   list-style: none;
                    693:   min-height: 1em;
                    694:   margin-top: 0em;
                    695:   margin-bottom: 0em;
                    696:   margin-left: 0em;
                    697:   padding-left: 1.5em;
                    698: }
                    699: 
                    700: img.bullet {
                    701:   cursor: default;
                    702: }
                    703: 
                    704: /* DNWList */
                    705: ul.wlist>li.selected {
                    706:   color: inherit;
                    707: }
                    708: ul.wlist>li.selected span {
                    709:   color: #FFFFFF;
                    710: }
                    711: 
                    712: /* DNTable */
                    713: div.table>table {
                    714:   width: 100%;
                    715:   border-collapse: collapse;
                    716:   border: 1px solid #000000;
                    717:   border-spacing: 0px;
                    718:   box-shadow: 2px 2px 2px #A0A0A0;
                    719:   margin-bottom: 2px;
                    720: }
                    721: 
                    722: div.table>table>tr>td {
                    723:   min-width: 2em;
                    724:   border: 1px solid #000000;
                    725:   word-break: break-all;
                    726:   padding: 2px;
                    727: }
                    728: 
                    729: form.table_buttons {
                    730:   padding: 1px;
                    731:   background-color: #E0E0E0;
                    732:   border-top: 1px solid #000000;
                    733:   border-left: 1px solid #000000;
                    734:   border-right: 1px solid #000000;
                    735:   box-shadow: 2px 0px 2px #A0A0A0;
                    736:   font-family: sans-serif;
                    737:   font-weight: normal;
                    738:   font-style: normal;
                    739:   font-size: medium;
                    740:   text-align: left;
                    741:   color: black;
                    742: }
                    743: 
                    744: td.header {
                    745:   font-weight: bold;
                    746: }
                    747: 
                    748: /* DNFile */
                    749: img.dn {
                    750:   cursor: default;
                    751: }
                    752: 
                    753: img.dn.selected, .selected img.dn {
                    754:   opacity: 0.7;
                    755: }
                    756: 
                    757: /* DNSpecial */
                    758: span.special {
                    759:   font-family: STIXSubset-Regular;
                    760: }
                    761: 
                    762: table.special_dlg {
                    763:   font-family: STIXSubset-Regular;
                    764:   cursor: default;
                    765: }
                    766: 
                    767: /* DNForm */
                    768: td.shrink {
                    769:   white-space: nowrap;
                    770: }
                    771: .expand {
                    772:   width: 99%;
                    773: }
                    774: span.form_title {
                    775:   position: relative;
                    776:   top: 3px;
                    777:   border-top: 1px solid #505050;
                    778:   border-left: 1px solid #505050;
                    779:   border-right: 1px solid #505050;
                    780:   padding-left: 4px;
                    781:   padding-right: 4px;
                    782:   padding-top: 2px;
                    783:   padding-bottom: 2px;
                    784:   background-color: #F0F0F0;
                    785:   border-top-left-radius: 0.4em;
                    786:   border-top-right-radius: 0.4em;
                    787: }
                    788: 
                    789: .selected span.form_title {
                    790:   background-color: #50A0FF;
                    791: }
                    792: 
                    793: div.form {
                    794:   font-family: sans-serif;
                    795:   font-weight: normal;
                    796:   font-style: normal;
                    797:   font-size: medium;
                    798:   text-align: left;
                    799:   color: black;
                    800: }
                    801: 
                    802: div.form table {
                    803:   border: 1px solid #505050;
                    804:   border-spacing: 0px;
                    805:   box-shadow: 2px 2px 2px #A0A0A0;
                    806:   margin-bottom: 2px;
                    807:   background-color: #F5F5F5;
                    808:   border-top-right-radius: 0.4em;
                    809:   border-bottom-right-radius: 0.4em;
                    810:   border-bottom-left-radius: 0.4em;
                    811: }
                    812: 
                    813: .selected div.form table,  div.form.selected table {
                    814:   background-color: #50A0FF;
                    815: }
                    816: 
                    817: div.form td {
                    818:   padding-left: 3px;
                    819:   padding-right: 3px;
                    820: }
                    821: 
                    822: /* DNFormField */
                    823: .form_field {
                    824:   width: 100%;
                    825:   min-height: 1em;
                    826:   background-color: white;
                    827:   border-top: 2px solid #A0A0A0;
                    828:   border-left: 2px solid #A0A0A0;
                    829:   border-right: 2px solid #F5F5F5;
                    830:   border-bottom: 2px solid #F5F5F5;
                    831: }
                    832: 
                    833: 
                    834: select.invalid {
                    835:   border: 1px solid #F00000;
                    836: }
                    837: 
                    838: /* DNSimpleType */
                    839: span.simple_type {
                    840:   padding: 3px;
                    841: }
                    842: 
                    843: /* Fonts for symbols and equations */
                    844: 
                    845: @font-face { 
                    846:     font-family: 'STIXSubset-Regular';
                    847:     src: url('fonts/STIXSubset-Regular.eot');
                    848:     src: local('STIXSubset-Regular'), url('fonts/STIXSubset-Regular.ttf') format('truetype');
                    849: }
                    850: 
                    851: @font-face { 
                    852:     font-family: 'STIXSubset-Bold';
                    853:     src: url('fonts/STIXSubset-Bold.eot');
                    854:     src: local('STIXSubset-Bold'), url('fonts/STIXSubset-Bold.ttf') format('truetype');
                    855: }
                    856: 
                    857: @font-face { 
                    858:     font-family: 'STIXSubset-Italic';
                    859:     src: url('fonts/STIXSubset-Italic.eot');
                    860:     src: local('STIXSubset-Italic'), url('fonts/STIXSubset-Italic.ttf') format('truetype');
                    861: }
                    862: 
                    863: span.symbol {
                    864:     font-family: STIXSubset-Regular, "Times New Roman", Times, serif;
                    865: }

FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>