extra.css 1.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124
  1. body {
  2. text-align: justify;
  3. }
  4. h1 {
  5. line-height: 110%;
  6. }
  7. .hlist {
  8. border: 1px solid navy;
  9. padding:5px;
  10. background-color: #F4FFFF;
  11. }
  12. .hlist li {
  13. display: inline;
  14. display: inline-table;
  15. list-style-type: none;
  16. padding-right: 20px;
  17. }
  18. .entity {
  19. border: 1px solid navy;
  20. margin:5px 0px 5px 0px;
  21. padding: 5px;
  22. }
  23. .type-c {
  24. cursor:help;
  25. color:orange;
  26. }
  27. .type-op {
  28. cursor:help;
  29. color:navy;
  30. }
  31. .type-dp {
  32. cursor:help;
  33. color:green;
  34. }
  35. .type-ap {
  36. cursor:help;
  37. color:maroon;
  38. }
  39. .type-ni {
  40. cursor:help;
  41. color:brown;
  42. }
  43. .logic {
  44. color:purple;
  45. font-weight:bold;
  46. }
  47. h3 {
  48. margin-top: 3px;
  49. padding-bottom: 5px;
  50. border-bottom: 1px solid navy;
  51. }
  52. h2 {
  53. margin-top:40px;
  54. }
  55. .dotted {
  56. border-bottom: 1px dotted gray;
  57. }
  58. dt {
  59. margin-top:5px;
  60. }
  61. .description {
  62. border-top: 1px dashed gray;
  63. border-bottom: 1px dashed gray;
  64. background-color: rgb(242, 243, 244);
  65. margin-top:5px;
  66. padding-bottom:5px;
  67. }
  68. .description dl {
  69. background-color: rgb(242, 243, 244);
  70. }
  71. .description ul {
  72. padding-left: 12px;
  73. margin-top: 0px;
  74. }
  75. .backlink {
  76. font-size:10pt;
  77. text-align:right;
  78. float:right;
  79. color:black;
  80. padding: 2px;
  81. border: 1px dotted navy;
  82. background-color: #F4FFFF;
  83. }
  84. .imageblock {
  85. text-align: center;
  86. }
  87. .imageblock img {
  88. border:1px solid gray;
  89. }
  90. .endnote {
  91. margin-top: 40px;
  92. border-top: 1px solid gray;
  93. padding-top: 10px;
  94. text-align: center;
  95. color:gray;
  96. font-size:70%;
  97. }
  98. .literal {
  99. color:green;
  100. font-style:italic;
  101. }