1
+ /* styling for all html tags */
1
2
body {
2
3
background : # ccc ;
3
4
color : grey;
6
7
table {
7
8
font-size : 0.9em ;
8
9
}
10
+ pre {
11
+ overflow : visible !important ;
12
+ }
13
+
14
+ /* styling for generic classes */
15
+ .pre {
16
+ white-space : pre;
17
+ }
18
+ .monospace {
19
+ font-family : monospace;
20
+ }
9
21
.lighttext {
10
22
color : # 4a4a4a ;
11
23
}
12
24
.glyphicon {
13
25
/* glyphicons are too bold, make them lighter*/
14
26
color : # 848484 ;
15
27
}
28
+ .flex {
29
+ display : flex;
30
+ }
31
+ /* components get their own titlebars */
16
32
.titlebar {
17
33
width : 100% ;
18
34
color : black;
19
35
background-color : white;
20
36
}
21
- # console , .gdb_console {
37
+ .pointer {
38
+ cursor : pointer;
39
+ }
40
+ .gdb_content_div {
41
+ overflow : auto;
42
+ height : 150px ;
43
+ background-color : # f7f7f7 ;
44
+ border-color : grey;
45
+ border-style : solid;
46
+ border-width : 1px ;
47
+ border-radius : 2px ;
48
+ }
49
+
50
+ /* specific styling for ids */
51
+ # always_on_top {
52
+ position : fixed;
53
+ top : 0 ;
54
+ margin-top : 0 ;
55
+ height : 102px ;
56
+ width : 100% ;
57
+ border-bottom : black;
58
+ border-style : solid;
59
+ border-width : 0px ;
60
+ border-bottom-width : 1px ;
61
+ z-index : 1000 ;
62
+ background : # f1f1f1 ;
63
+ border-bottom-color : # ccc ;
64
+ }
65
+ # console {
22
66
font-size : 0.9em !important ;
23
67
background-color : # 292929 !important ;
24
68
color : # f9f9f9 !important ;
25
69
font-family : monospace !important ;
26
70
}
27
- # stdout {
28
- color : black;
71
+ # gdb_command {
72
+ padding-left : 45px ;
73
+ border-top : 0 ;
74
+ border-top-left-radius : 0 ;
75
+ border-top-right-radius : 0 ;
76
+ font-size : 0.9em !important ;
77
+ background-color : # 3c3c3c !important ;
78
+ color : # f9f9f9 !important ;
79
+ font-family : monospace !important ;
29
80
}
30
- # console , # stdout , # gdb_mi_output {
81
+ # gdb_mi_output {
31
82
font-family : monospace;
32
83
overflow : auto;
33
84
font-size : 0.9em ;
34
85
}
35
- .pointer {
36
- cursor : pointer;
37
- }
38
86
.sent_command : hover {
39
87
/* lighten background */
40
- background-color : rgba (255 , 255 , 255 , 0.5 )
88
+ background-color : rgba (255 , 255 , 255 , 0.1 )
41
89
}
42
90
.disabled {
43
91
z-index : 1000 ;
44
92
background-color : lightgrey;
45
93
opacity : 0.6 ;
46
94
pointer-events : none;
47
95
}
48
- .no_margin {
96
+ .margin_sm {
49
97
margin : 2px ;
50
98
}
51
99
.no_padding {
52
100
padding : 2px !important ;
53
101
}
54
- .code {
55
- overflow : auto;
56
- font-size : 0.9em ;
57
- }
58
102
.code pre , table .code {
59
103
margin : 0px ;
60
104
padding : 0px ;
@@ -64,67 +108,60 @@ table{
64
108
.highlight {
65
109
background : rgba (255 , 255 , 0 , 0.5 );
66
110
}
67
- .breakpoint td .gutter div {
68
- background : blue;
69
- width : 0.9em ;
70
- height : 0.9em ;
71
- border-radius : 50% ;
72
- border-color : black;
73
- }
74
- .no_breakpoint td .gutter div {
75
- /*background: blue;*/
76
- width : 0.9em ;
77
- height : 0.9em ;
78
- border-radius : 50% ;
79
- border-color : black;
111
+ .line_num_container {
112
+ width : 50px ;
113
+ border-width : 0 ;
114
+ border-right : 1px ;
115
+ border-style : solid;
116
+ border-color : # c7c7c7 ;
80
117
}
81
- .active_breakpoint {
82
- background : red;
118
+ .line_num {
119
+ padding-left : 10px ;
120
+ padding-right : 10px ;
121
+ font-family : monospace;
122
+ font-size : 0.9em ;
123
+ color : # ababab ;
124
+ cursor : pointer;
83
125
}
84
- .gutter {
85
- width : 0.9em ;
86
- padding-right : 5px ;
87
- background : # d4ffab ;
126
+ /* the line number has its style changed if it has a breakpoint */
127
+ .line_num .breakpoint {
128
+ background : # 33cdff ;
129
+ color : black;
130
+ border-style : solid;
131
+ border-color : # 000000 ;
132
+ border-width : 1px ;
88
133
}
89
- .pre {
90
- white-space : pre;
134
+ /* set background color over souce code only */
135
+ .source_code_row .line_of_code td {
136
+ background-color : # f7f7f7 ;
91
137
}
92
- pre {
93
- overflow : visible !important ;
138
+ . line_of_code pre {
139
+ margin-left : 10 px ;
94
140
}
95
- .source_code : hover td , .source_code : hover td pre {
141
+ /* when hovering, set background color of entire row */
142
+ .source_code_row : hover td , .source_code_row : hover td pre {
96
143
background-color : lightblue;
97
- cursor : pointer;
98
- }
99
- .source_code td {
100
- background-color : # f7f7f7
101
144
}
102
145
.padding_left {
103
146
padding-left : 5px ;
104
147
}
105
148
.line_of_code {
106
149
height : 18px
107
150
}
108
- .gdb_content_div {
109
- overflow : auto;
110
- height : 150px ;
111
- background-color : # f7f7f7 ;
112
- border-color : grey;
113
- border-style : solid;
114
- border-width : 1px ;
115
- border-radius : 2px ;
116
- }
117
151
.dropdown-btn {
118
152
vertical-align : top;
119
153
height : 30px ;
120
154
border-top-left-radius : 0 ;
121
155
border-bottom-left-radius : 0 ;
122
156
}
157
+ /* auto-complete librarie's dropdown should only be 200px high, and should
158
+ have scrollbar, so it doesn't take over the page */
123
159
.awesomplete ul {
124
160
overflow : auto;
125
161
max-height : 200px ;
126
162
}
127
163
164
+ /* show a flash of color */
128
165
.flash {
129
166
-webkit-animation-name : flash-animation;
130
167
-webkit-animation-duration : 1.0s ;
@@ -142,3 +179,18 @@ pre{
142
179
from { background : yellow; }
143
180
to { background : default; }
144
181
}
182
+
183
+ # variables li {
184
+ list-style : none;
185
+ }
186
+
187
+ # variables ul .variable {
188
+ padding-left : 5px ;
189
+ border : 0px ;
190
+ }
191
+ # variables li : hover {
192
+ background-color : # c0eeff ;
193
+ }
194
+ .toggle_children_visibility {
195
+ font-weight : bold;
196
+ }
0 commit comments