aboutsummaryrefslogtreecommitdiffstats
path: root/language-web/src/main
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2021-07-05 14:43:51 +0200
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2021-07-05 14:43:51 +0200
commitb023fa155e066af953ff7b456f68a39c8cce1ebb (patch)
treeb1435d76116fcd57f42b30a538b4201612d82279 /language-web/src/main
parentFix typo in environmental variable name (diff)
downloadrefinery-b023fa155e066af953ff7b456f68a39c8cce1ebb.tar.gz
refinery-b023fa155e066af953ff7b456f68a39c8cce1ebb.tar.zst
refinery-b023fa155e066af953ff7b456f68a39c8cce1ebb.zip
Appearance fixes
Diffstat (limited to 'language-web/src/main')
-rw-r--r--language-web/src/main/css/index.scss26
-rw-r--r--language-web/src/main/js/editor/EditorButtons.jsx13
-rw-r--r--language-web/src/main/js/editor/EditorStore.jsx6
-rw-r--r--language-web/src/main/js/index.jsx1
4 files changed, 35 insertions, 11 deletions
diff --git a/language-web/src/main/css/index.scss b/language-web/src/main/css/index.scss
index 319dff8d..3ed91824 100644
--- a/language-web/src/main/css/index.scss
+++ b/language-web/src/main/css/index.scss
@@ -23,15 +23,37 @@ body {
23 font-family: 'Roboto', sans-serif; 23 font-family: 'Roboto', sans-serif;
24} 24}
25 25
26.CodeMirror {
27 height: 100%;
28}
29
26.CodeMirror, .CodeMirror-hints { 30.CodeMirror, .CodeMirror-hints {
27 font-size: 16px; 31 font-size: 16px;
28 height: 100%;
29 font-family: 'JetBrains MonoVariable', 'JetBrains Mono', monospace; 32 font-family: 'JetBrains MonoVariable', 'JetBrains Mono', monospace;
30 font-feature-settings: 'liga', 'calt'; 33 font-feature-settings: 'liga', 'calt';
31 font-weight: 400; 34 font-weight: 400;
32 text-rendering: optimizeLegibility; 35 text-rendering: optimizeLegibility;
33} 36}
34 37
38.CodeMirror-hints {
39 background: #333333;
40 border: 0;
41 border-radius: 4px;
42 box-shadow: 0 2px 4px -1px rgba(0, 0, 0, 0.2),
43 0 5px 8px 0 rgba(0, 0, 0, 0.14),
44 0 1px 8px 0 rgba(0, 0, 0, 0.12);
45 padding: 0;
46}
47
48.CodeMirror-hint {
49 color: #fff;
50 border-radius: 0;
51}
52
53li.CodeMirror-hint-active {
54 background: rgba(128, 203, 196, 0.2);
55}
56
35.annotations-gutter { 57.annotations-gutter {
36 width: 12px; 58 width: 12px;
37} 59}
@@ -118,5 +140,5 @@ body {
118} 140}
119 141
120.problem-singleton-variable { 142.problem-singleton-variable {
121 opacity: 0.7; 143 opacity: 0.6;
122} 144}
diff --git a/language-web/src/main/js/editor/EditorButtons.jsx b/language-web/src/main/js/editor/EditorButtons.jsx
index 422c8a6d..f67afdbf 100644
--- a/language-web/src/main/js/editor/EditorButtons.jsx
+++ b/language-web/src/main/js/editor/EditorButtons.jsx
@@ -13,17 +13,14 @@ import { useRootStore } from '../RootStore';
13 13
14const useStyles = makeStyles(theme => ({ 14const useStyles = makeStyles(theme => ({
15 iconButton: { 15 iconButton: {
16 padding: 8, 16 padding: 7,
17 minWidth: 36, 17 minWidth: 36,
18 border: 0,
19 color: theme.palette.text.primary,
18 '&.MuiButtonGroup-groupedTextHorizontal': { 20 '&.MuiButtonGroup-groupedTextHorizontal': {
19 borderRight: 0, 21 borderRight: 0,
20 }, 22 },
21 }, 23 },
22 flatToggleButton: {
23 padding: 8,
24 border: 0,
25 color: theme.palette.text.primary,
26 },
27 divider: { 24 divider: {
28 margin: theme.spacing(0.5), 25 margin: theme.spacing(0.5),
29 } 26 }
@@ -49,7 +46,7 @@ export default observer(() => {
49 disabled={!editorStore.canRedo} 46 disabled={!editorStore.canRedo}
50 onClick={() => editorStore.redo()} 47 onClick={() => editorStore.redo()}
51 className={classes.iconButton} 48 className={classes.iconButton}
52 aria-label='REdo' 49 aria-label='Redo'
53 > 50 >
54 <RedoIcon fontSize='small'/> 51 <RedoIcon fontSize='small'/>
55 </Button> 52 </Button>
@@ -63,7 +60,7 @@ export default observer(() => {
63 selected={editorStore.showLineNumbers} 60 selected={editorStore.showLineNumbers}
64 onChange={() => editorStore.toggleLineNumbers()} 61 onChange={() => editorStore.toggleLineNumbers()}
65 size='small' 62 size='small'
66 className={classes.flatToggleButton} 63 className={classes.iconButton}
67 aria-label='Show line numbers' 64 aria-label='Show line numbers'
68 > 65 >
69 <FormatListNumberedIcon fontSize='small'/> 66 <FormatListNumberedIcon fontSize='small'/>
diff --git a/language-web/src/main/js/editor/EditorStore.jsx b/language-web/src/main/js/editor/EditorStore.jsx
index 6b03b383..b6f9bc0a 100644
--- a/language-web/src/main/js/editor/EditorStore.jsx
+++ b/language-web/src/main/js/editor/EditorStore.jsx
@@ -9,6 +9,8 @@ export default class EditorStore {
9 value = ''; 9 value = '';
10 /** @type {boolean} */ 10 /** @type {boolean} */
11 showLineNumbers = false; 11 showLineNumbers = false;
12 /** @type {boolean} */
13 showLigatures = true;
12 14
13 constructor() { 15 constructor() {
14 this.atom = createAtom('EditorStore'); 16 this.atom = createAtom('EditorStore');
@@ -78,4 +80,8 @@ export default class EditorStore {
78 toggleLineNumbers() { 80 toggleLineNumbers() {
79 this.showLineNumbers = !this.showLineNumbers; 81 this.showLineNumbers = !this.showLineNumbers;
80 } 82 }
83
84 toggleLigatures() {
85 this.showLigatures = !this.showLigatures;
86 }
81} 87}
diff --git a/language-web/src/main/js/index.jsx b/language-web/src/main/js/index.jsx
index f6775760..b3277a30 100644
--- a/language-web/src/main/js/index.jsx
+++ b/language-web/src/main/js/index.jsx
@@ -51,7 +51,6 @@ const theme = createMuiTheme({
51 type: 'dark', 51 type: 'dark',
52 background: { 52 background: {
53 default: '#212121', 53 default: '#212121',
54 paper: '#333333',
55 }, 54 },
56 primary: { 55 primary: {
57 main: '#82aaff', 56 main: '#82aaff',