diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx index 813737c792e21cc1aaa3f5e59314bddbe0d0041d..de36f8f01b24b451ee042930a0735c67c5e3c69f 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 {