From eb576e3735233f96a230d86ac2bd7ee2a680b4be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 12 Sep 2023 19:41:20 +0200
Subject: [PATCH] [wp/ivette] status bar for server activity
---
ivette/src/frama-c/kernel/Status.tsx | 35 ++++++++++++++++---------
ivette/src/frama-c/plugins/wp/index.tsx | 8 +++---
2 files changed, 26 insertions(+), 17 deletions(-)
diff --git a/ivette/src/frama-c/kernel/Status.tsx b/ivette/src/frama-c/kernel/Status.tsx
index af26e3655c4..a8585ac8545 100644
--- a/ivette/src/frama-c/kernel/Status.tsx
+++ b/ivette/src/frama-c/kernel/Status.tsx
@@ -25,10 +25,8 @@
/* --------------------------------------------------------------------------*/
import React from 'react';
-import { Code } from 'dome/controls/labels';
+import { Code, IconKind } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
-import { LED } from 'dome/controls/displays';
-import { Icon } from 'dome/controls/icons';
import * as Toolbars from 'dome/frame/toolbars';
import { GlobalState, useGlobalState } from 'dome/data/states';
import * as Server from 'frama-c/server';
@@ -44,31 +42,42 @@ export interface MessageProps {
const emptyMessage: MessageProps = { text: '', kind: 'none' };
+
const GlobalMessage = new GlobalState(emptyMessage);
export function setMessage(message: MessageProps): void {
GlobalMessage.setValue(message);
}
+const msgIcon: { [kind: string]: string } = {
+ 'progress': 'EXECUTE',
+ 'success': 'CHECK',
+ 'warning': 'WARNING',
+ 'error': 'CROSS',
+ 'info': 'HELP',
+};
+
+const msgKind: { [kind: string]: IconKind } = {
+ 'success': 'positive',
+ 'warning': 'warning',
+ 'error': 'negative',
+};
+
export default function Message(): JSX.Element {
const [message] = useGlobalState(GlobalMessage);
+ const icon = msgIcon[message.kind];
+ const kind = msgKind[message.kind];
return (
- <>
- <Toolbars.Space />
- {message.kind === 'progress' && <LED status="active" blink />}
- {message.kind === 'success' && <Icon id="CHECK" fill="green" />}
- {message.kind === 'warning' && <Icon id="ATTENTION" />}
- {message.kind === 'error' && <Icon id="CROSS" fill="red" />}
- {message.kind === 'info' && <Icon id="CIRC.INFO" />}
- <Code label={message.text} title={message.title} />
+ <Toolbars.Group display={message.kind !== 'none'} >
+ <Code icon={icon} kind={kind}
+ label={message.text} title={message.title} />
<IconButton
icon="CIRC.CLOSE"
onClick={() => setMessage(emptyMessage)}
visible={message !== emptyMessage}
title="Hide current message"
/>
- <Toolbars.Space />
- </>
+ </Toolbars.Group>
);
}
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index d748d75a3a4..ebc87c0fc24 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -29,7 +29,7 @@ import * as Dome from 'dome';
import { Label } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
import { LED, Meter } from 'dome/controls/displays';
-import { Inset } from 'dome/frame/toolbars';
+import { Group, Inset } from 'dome/frame/toolbars';
import * as Ivette from 'ivette';
import * as States from 'frama-c/states';
import { GoalTable } from './goals';
@@ -91,12 +91,12 @@ function ServerActivity(): JSX.Element {
const todo = rq ? rq.todo : 0;
const total = done + todo;
return (
- <>
+ <Group display={total > 0}>
<LED status={status} />
- <Label>WP {done} / {total}</Label>
+ <Label>WP</Label>
<Meter value={done} min={0} max={done + total} />
<Inset />
- </>
+ </Group>
);
}
--
GitLab