annotate src/nabble/view/web/util/codemirror/css/docs.css @ 62:4674ed7d56df default tip

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