diff options
Diffstat (limited to 'language-web/src/main/css/index.scss')
-rw-r--r-- | language-web/src/main/css/index.scss | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/language-web/src/main/css/index.scss b/language-web/src/main/css/index.scss index 9d6e0f6a..54f3a654 100644 --- a/language-web/src/main/css/index.scss +++ b/language-web/src/main/css/index.scss | |||
@@ -30,12 +30,27 @@ body { | |||
30 | height: 100%; | 30 | height: 100%; |
31 | } | 31 | } |
32 | 32 | ||
33 | .CodeMirror, .CodeMirror-hints { | 33 | .problem-fallback-editor { |
34 | display: block; | ||
35 | height: 100%; | ||
36 | width: 100%; | ||
37 | resize: none; | ||
38 | border: none; | ||
39 | outline: none; | ||
40 | padding: 4px 4px 4px 16px; | ||
41 | white-space: pre; | ||
42 | overflow-wrap: normal; | ||
43 | overflow: auto; | ||
44 | } | ||
45 | |||
46 | .CodeMirror, .CodeMirror-hints, .problem-fallback-editor { | ||
34 | font-size: 16px; | 47 | font-size: 16px; |
35 | font-family: 'JetBrains MonoVariable', 'JetBrains Mono', monospace; | 48 | font-family: 'JetBrains MonoVariable', 'JetBrains Mono', monospace; |
36 | font-feature-settings: 'liga', 'calt'; | 49 | font-feature-settings: 'liga', 'calt'; |
37 | font-weight: 400; | 50 | font-weight: 400; |
38 | text-rendering: optimizeLegibility; | 51 | text-rendering: optimizeLegibility; |
52 | line-height: 1.35; | ||
53 | letter-spacing: 0; | ||
39 | } | 54 | } |
40 | 55 | ||
41 | @each $themeName, $theme in $themes { | 56 | @each $themeName, $theme in $themes { |
@@ -45,6 +60,16 @@ body { | |||
45 | color: map.get($theme, 'foreground'); | 60 | color: map.get($theme, 'foreground'); |
46 | } | 61 | } |
47 | 62 | ||
63 | &.problem-fallback-editor { | ||
64 | background: map.get($theme, 'background'); | ||
65 | color: map.get($theme, 'foreground'); | ||
66 | caret-color: map.get($theme, 'cursor'); | ||
67 | |||
68 | &::selection { | ||
69 | background: map.get($theme, 'selection'); | ||
70 | } | ||
71 | } | ||
72 | |||
48 | .CodeMirror-gutters { | 73 | .CodeMirror-gutters { |
49 | background: map.get($theme, 'background'); | 74 | background: map.get($theme, 'background'); |
50 | border: none; | 75 | border: none; |
@@ -183,11 +208,13 @@ li.CodeMirror-hint-active { | |||
183 | 208 | ||
184 | .xtext-marker_read { | 209 | .xtext-marker_read { |
185 | background: rgba(128, 203, 196, 0.2); | 210 | background: rgba(128, 203, 196, 0.2); |
211 | display: inline-block; | ||
186 | } | 212 | } |
187 | 213 | ||
188 | 214 | ||
189 | .xtext-marker_write { | 215 | .xtext-marker_write { |
190 | background: rgba(255, 229, 100, 0.2); | 216 | background: rgba(255, 229, 100, 0.2); |
217 | display: inline-block; | ||
191 | } | 218 | } |
192 | 219 | ||
193 | .problem-abstract { | 220 | .problem-abstract { |