1// disable gutter
2$grid-gutter-width: 0;
3
4$base-font-size: 1rem;
5$font-family-monospace: monospace;
6$headings-margin-bottom: 0;
7
8// basic functionality
9@import "bootstrap/scss/_functions.scss";
10@import "bootstrap/scss/_variables.scss";
11@import "bootstrap/scss/_variables-dark.scss";
12@import "bootstrap/scss/_maps.scss";
13@import "bootstrap/scss/_mixins.scss";
14@import "bootstrap/scss/_utilities.scss";
15
16// added component
17@import "bootstrap/scss/_root.scss";
18@import "bootstrap/scss/_containers.scss";
19@import "bootstrap/scss/_nav.scss";
20@import "bootstrap/scss/_navbar.scss";
21@import "bootstrap/scss/_grid.scss";
22@import "tree.scss";
23
24// TODO remove once is not needed
25$alert-border-radius: 0;
26@import "bootstrap/scss/_alert.scss";
27
28// overwrite to reduce the ammount of css generated by loading all utilities
29$utilities: (
30 "order": (
31 responsive: true,
32 property: order,
33 values: (
34 first: -1,
35 0: 0,
36 1: 1,
37 2: 2,
38 3: 3,
39 4: 4,
40 5: 5,
41 last: 6,
42 ),
43 ),
44 "float": (
45 responsive: true,
46 property: float,
47 values: (
48 start: left,
49 end: right,
50 none: none,
51 )
52 ),
53 "text-align": (
54 responsive: true,
55 property: text-align,
56 class: text,
57 values: (
58 start: left,
59 end: right,
60 center: center,
61 )
62),
63);
64
65@import "bootstrap/scss/utilities/_api.scss";
66
67body {
68 // prevents wierd font resizing on overflow
69 -webkit-text-size-adjust: 100%;
70 font-family: $font-family-monospace;
71 font-size: $base-font-size;
72 margin: 0;
73}
74
75.navbar-nav {
76 margin-top: 0px
77}
78
79.event-list {
80 margin-bottom: 1rem;
81}
82
83.event:first-child {
84 margin-top: 0;
85}
86
87.event {
88 text-overflow: ellipsis;
89 overflow: hidden;
90 padding: 0.5rem;
91 margin: 0.5rem 0;
92 background: #f8f9fa;
93}
94
95.selected {
96 text-decoration: underline;
97}
98
99.event > h4 {
100 margin: 0;
101}
102.event > p {
103 margin: 0.5rem 0;
104}
105
106.code-view {
107 display: grid;
108 overflow-x: auto;
109}
110
111.logs {
112 >div {
113 background: #f8f9fa;
114 }
115
116 >div {
117 padding: 5px;
118 margin: $spacer;
119 }
120
121 @include media-breakpoint-down(md) {
122 >div {
123 margin: $spacer 0 $spacer 0;
124 }
125 }
126
127 pre {
128 font-size: $base-font-size;
129 margin: 0;
130 }
131}
132
133.logs>div>div:first-child {
134 margin-bottom: 15px;
135}
136.logs>div>div:last-child {
137 margin-top: 15px;
138}
139
140#about {
141 padding: 0 $spacer $spacer $spacer;
142 > p:first-child {
143 margin-top: 0
144 }
145
146 @include media-breakpoint-down(md) {
147 padding: $spacer;
148 max-width: calc(100% - calc(2 * #{$spacer}));
149 }
150}