From 80fe5092b9099a87b9811b865a21ae8edf5f32ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 23 Mar 2022 16:28:22 +0100
Subject: [PATCH] [ivette] Richtext: fixes Text component.
Do not modify the text argument in-place!
Uses array.map instead of React.Children.map.
---
ivette/src/frama-c/richtext.tsx | 19 ++++++-------------
1 file changed, 6 insertions(+), 13 deletions(-)
diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx
index 813737c792e..de36f8f01b2 100644
--- a/ivette/src/frama-c/richtext.tsx
+++ b/ivette/src/frama-c/richtext.tsx
@@ -98,26 +98,19 @@ function Marker(props: MarkerProps): JSX.Element {
function makeContents(text: KernelData.text): React.ReactNode {
if (Array.isArray(text)) {
- const tag = text.shift();
- let marker: string | undefined;
- if (tag) {
- if (Array.isArray(tag)) {
- text.unshift(tag);
- } else if (typeof tag === 'string') {
- marker = tag;
- }
- // otherwize, ignore tag
+ const tag = text[0];
+ const marker = tag && typeof (tag) === 'string';
+ const array = marker ? text.slice(1) : text;
+ const contents = React.Children.toArray(array.map(makeContents));
+ if (marker) {
+ return <Marker marker={tag}>{contents}</Marker>;
}
- const contents = React.Children.map(text, makeContents);
- if (marker)
- return <Marker marker={marker}>{contents}</Marker>;
return <>{contents}</>;
} if (typeof text === 'string') {
return text;
}
D.error('Unexpected text', text);
return null;
-
}
export interface TextProps {
--
GitLab