diff options
author | 2023-08-20 19:41:32 +0200 | |
---|---|---|
committer | 2023-08-20 20:29:02 +0200 | |
commit | a3f1e6872f4f768d14899a1e70bbdc14f32e478d (patch) | |
tree | b2daf0c81724f31ee190f5d63eb42988086dabf2 /subprojects/frontend/src/editor/AnimatedButton.tsx | |
parent | fix: nullary model initialization (diff) | |
download | refinery-a3f1e6872f4f768d14899a1e70bbdc14f32e478d.tar.gz refinery-a3f1e6872f4f768d14899a1e70bbdc14f32e478d.tar.zst refinery-a3f1e6872f4f768d14899a1e70bbdc14f32e478d.zip |
feat: improve semantics error reporting
Also makes model seeds cancellable to reduce server load during semantic
analysis.
Diffstat (limited to 'subprojects/frontend/src/editor/AnimatedButton.tsx')
-rw-r--r-- | subprojects/frontend/src/editor/AnimatedButton.tsx | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/subprojects/frontend/src/editor/AnimatedButton.tsx b/subprojects/frontend/src/editor/AnimatedButton.tsx index dbbda618..24ec69be 100644 --- a/subprojects/frontend/src/editor/AnimatedButton.tsx +++ b/subprojects/frontend/src/editor/AnimatedButton.tsx | |||
@@ -48,7 +48,7 @@ export default function AnimatedButton({ | |||
48 | onClick?: () => void; | 48 | onClick?: () => void; |
49 | color: 'error' | 'warning' | 'primary' | 'inherit'; | 49 | color: 'error' | 'warning' | 'primary' | 'inherit'; |
50 | disabled?: boolean; | 50 | disabled?: boolean; |
51 | startIcon: JSX.Element; | 51 | startIcon?: JSX.Element; |
52 | sx?: SxProps<Theme> | undefined; | 52 | sx?: SxProps<Theme> | undefined; |
53 | children?: ReactNode; | 53 | children?: ReactNode; |
54 | }): JSX.Element { | 54 | }): JSX.Element { |
@@ -79,7 +79,11 @@ export default function AnimatedButton({ | |||
79 | className="rounded shaded" | 79 | className="rounded shaded" |
80 | disabled={disabled ?? false} | 80 | disabled={disabled ?? false} |
81 | startIcon={startIcon} | 81 | startIcon={startIcon} |
82 | width={width === undefined ? 'auto' : `calc(${width} + 50px)`} | 82 | width={ |
83 | width === undefined | ||
84 | ? 'auto' | ||
85 | : `calc(${width} + ${startIcon === undefined ? 28 : 50}px)` | ||
86 | } | ||
83 | > | 87 | > |
84 | <Box | 88 | <Box |
85 | display="flex" | 89 | display="flex" |
@@ -100,6 +104,7 @@ AnimatedButton.defaultProps = { | |||
100 | 'aria-label': undefined, | 104 | 'aria-label': undefined, |
101 | onClick: undefined, | 105 | onClick: undefined, |
102 | disabled: false, | 106 | disabled: false, |
107 | startIcon: undefined, | ||
103 | sx: undefined, | 108 | sx: undefined, |
104 | children: undefined, | 109 | children: undefined, |
105 | }; | 110 | }; |