codemirror-additions.css 2.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172
  1. .CodeMirror {
  2. height: auto;
  3. }
  4. body {
  5. font-family: Droid Sans, Arial, sans-serif;
  6. line-height: 1.5;
  7. max-width: 64.3em;
  8. margin: 3em auto;
  9. padding: 0 1em;
  10. }
  11. h1 {
  12. letter-spacing: -3px;
  13. font-size: 3.23em;
  14. font-weight: bold;
  15. margin: 0;
  16. }
  17. h2 {
  18. font-size: 1.23em;
  19. font-weight: bold;
  20. margin: .5em 0;
  21. letter-spacing: -1px;
  22. }
  23. h3 {
  24. font-size: 1.1em;
  25. font-weight: bold;
  26. margin: .4em 0;
  27. }
  28. pre {
  29. background-color: #eee;
  30. -moz-border-radius: 6px;
  31. -webkit-border-radius: 6px;
  32. border-radius: 6px;
  33. padding: 1em;
  34. }
  35. pre.code {
  36. margin: 0 1em;
  37. }
  38. .grey {
  39. background-color: #eee;
  40. border-radius: 6px;
  41. margin-bottom: 1.65em;
  42. margin-top: 0.825em;
  43. padding: 0.825em 1.65em;
  44. position: relative;
  45. }
  46. img.logo {
  47. position: absolute;
  48. right: -1em;
  49. bottom: 4px;
  50. max-width: 23.6875em; /* Scale image down with text to prevent clipping */
  51. }
  52. .grey > pre {
  53. background:none;
  54. border-radius:0;
  55. padding:0;
  56. margin:0;
  57. font-size:2.2em;
  58. line-height:1.2em;
  59. }
  60. a:link, a:visited, .quasilink {
  61. color: #df0019;
  62. cursor: pointer;
  63. text-decoration: none;
  64. }
  65. a:hover, .quasilink:hover {
  66. color: #800004;
  67. }
  68. h1 a:link, h1 a:visited, h1 a:hover {
  69. color: black;
  70. }
  71. ul {
  72. margin: 0;
  73. padding-left: 1.2em;
  74. }
  75. a.download {
  76. color: white;
  77. background-color: #df0019;
  78. width: 100%;
  79. display: block;
  80. text-align: center;
  81. font-size: 1.23em;
  82. font-weight: bold;
  83. text-decoration: none;
  84. -moz-border-radius: 6px;
  85. -webkit-border-radius: 6px;
  86. border-radius: 6px;
  87. padding: .5em 0;
  88. margin-bottom: 1em;
  89. }
  90. a.download:hover {
  91. background-color: #bb0010;
  92. }
  93. .rel {
  94. margin-bottom: 0;
  95. }
  96. .rel-note {
  97. color: #777;
  98. font-size: .9em;
  99. margin-top: .1em;
  100. }
  101. .logo-braces {
  102. color: #df0019;
  103. position: relative;
  104. top: -4px;
  105. }
  106. .blk {
  107. float: left;
  108. }
  109. .left {
  110. margin-right: 20.68em;
  111. max-width: 37em;
  112. padding-right: 6.53em;
  113. padding-bottom: 1em;
  114. }
  115. .left1 {
  116. width: 15.24em;
  117. padding-right: 6.45em;
  118. }
  119. .left2 {
  120. max-width: 15.24em;
  121. }
  122. .right {
  123. width: 20.68em;
  124. margin-left: -20.68em;
  125. }
  126. .leftbig {
  127. width: 42.44em;
  128. padding-right: 6.53em;
  129. }
  130. .rightsmall {
  131. width: 15.24em;
  132. }
  133. .clear:after {
  134. visibility: hidden;
  135. display: block;
  136. font-size: 0;
  137. content: " ";
  138. clear: both;
  139. height: 0;
  140. }
  141. .clear { display: inline-block; }
  142. /* start commented backslash hack \*/
  143. * html .clear { height: 1%; }
  144. .clear { display: block; }
  145. /* close commented backslash hack */