From 7558ac03e789191ef168cc7dcbbb5ffa243bed84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Sun, 7 Apr 2024 17:27:48 +0200
Subject: [PATCH] [ivette] move Status to Display
---
ivette/src/frama-c/index.tsx | 2 -
ivette/src/frama-c/kernel/Locations.tsx | 44 ++++-----
ivette/src/frama-c/kernel/PivotTable.tsx | 18 ++--
ivette/src/frama-c/kernel/Status.tsx | 97 -------------------
ivette/src/frama-c/menu.ts | 27 +-----
ivette/src/frama-c/plugins/eva/valuetable.tsx | 17 ++--
ivette/src/frama-c/plugins/studia/index.ts | 11 +--
ivette/src/ivette/display.tsx | 16 ++-
ivette/src/ivette/prefs.tsx | 2 +-
9 files changed, 58 insertions(+), 176 deletions(-)
delete mode 100644 ivette/src/frama-c/kernel/Status.tsx
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index 5df09f7389c..5956727d634 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -29,7 +29,6 @@ import * as Ivette from 'ivette';
import History from 'frama-c/kernel/History';
import { Functions, Globals, Types } from 'frama-c/kernel/Globals';
-import Status from 'frama-c/kernel/Status';
import ASTview from 'frama-c/kernel/ASTview';
import ASTinfo from 'frama-c/kernel/ASTinfo';
import SourceCode from 'frama-c/kernel/SourceCode';
@@ -58,7 +57,6 @@ Ivette.registerSidebar({
});
Ivette.registerToolbar({ id: 'ivette.history', children: <History /> });
-Ivette.registerStatusbar({ id: 'ivette.status', children: <Status /> });
/* -------------------------------------------------------------------------- */
/* --- Frama-C Kernel Groups --- */
diff --git a/ivette/src/frama-c/kernel/Locations.tsx b/ivette/src/frama-c/kernel/Locations.tsx
index 557865901c8..7a4298db2da 100644
--- a/ivette/src/frama-c/kernel/Locations.tsx
+++ b/ivette/src/frama-c/kernel/Locations.tsx
@@ -36,7 +36,6 @@ import { Space } from 'dome/frame/toolbars';
import { TitleBar } from 'ivette';
import * as Display from 'ivette/display';
import * as Ast from 'frama-c/kernel/api/ast';
-import * as Status from 'frama-c/kernel/Status';
import * as Server from 'frama-c/server';
// --------------------------------------------------------------------------
@@ -61,20 +60,16 @@ export function useSelection(): MultiSelection {
return s;
}
-export function setSelection(s: MultiSelection): void
-{
+export function setSelection(s: MultiSelection): void {
MultiSelection.setValue(s);
const marker = s.index !== undefined ? s.markers[s.index] : undefined;
if (marker) States.setSelected(marker);
if (s.plugin && s.markers.length > 0) {
- const text =
+ const label =
`${s.plugin}: ${s.markers.length} locations selected, \
listed in the 'Locations' panel`;
const title = `${s.label}: ${s.markers.length} locations selected`;
- Status.setMessage({
- text, title,
- kind: 'success'
- });
+ Display.showMessage({ label, title });
Display.alertComponent('fc.kernel.locations');
}
}
@@ -86,16 +81,14 @@ export function setIndex(index: number): void {
setSelection({ ...s, index });
}
-function sameMarkers(xs: Ast.marker[], ys: Ast.marker[]): boolean
-{
+function sameMarkers(xs: Ast.marker[], ys: Ast.marker[]): boolean {
if (xs.length !== ys.length) return false;
for (let k = 0; k < xs.length; k++)
if (xs[k] !== ys[k]) return false;
return true;
}
-function sameSelection(u: MultiSelection, v: MultiSelection): boolean
-{
+function sameSelection(u: MultiSelection, v: MultiSelection): boolean {
if (u.label !== v.label) return false;
if (u.title !== v.title) return false;
return sameMarkers(u.markers, v.markers);
@@ -105,12 +98,11 @@ function sameSelection(u: MultiSelection, v: MultiSelection): boolean
Update the list of markers and select its first element,
or cycle to the next element wrt current selection.
*/
-export function setNextSelection(s: MultiSelection): void
-{
+export function setNextSelection(s: MultiSelection): void {
const selection = MultiSelection.getValue();
if (s.index === undefined && sameSelection(selection, s)) {
const { index, markers } = selection;
- const target = index === undefined ? 0 : index+1;
+ const target = index === undefined ? 0 : index + 1;
const select = target < markers.length ? target : 0;
setSelection({ ...selection, index: select });
} else {
@@ -143,14 +135,14 @@ class Model extends CompactModel<Ast.marker, Data> {
}
const renderIndex: Renderer<number> =
- (index) => <Cell label={`${index+1}`}/>;
+ (index) => <Cell label={`${index + 1}`} />;
const renderDecl: Renderer<Data> =
-(d) => {
- const name = d.decl.name;
- const label = d.decl.label;
- return <Cell label={name} title={label} />;
-};
+ (d) => {
+ const name = d.decl.name;
+ const label = d.decl.label;
+ return <Cell label={name} title={label} />;
+ };
const renderLocation: Renderer<Data> =
(d) => {
@@ -183,7 +175,7 @@ export default function LocationsTable(): JSX.Element {
const selected = index !== undefined ? markers[index] : undefined;
const size = markers.length;
const kindex = index === undefined ? (-1) : index;
- const indexLabel = index === undefined ? '…' : index+1;
+ const indexLabel = index === undefined ? '…' : index + 1;
const positionLabel = `${indexLabel} / ${size}`;
// Component
@@ -194,13 +186,13 @@ export default function LocationsTable(): JSX.Element {
icon='ANGLE.LEFT'
title='Previous location'
enabled={0 < kindex}
- onClick={() => gotoIndex(kindex-1)}
+ onClick={() => gotoIndex(kindex - 1)}
/>
<IconButton
icon='ANGLE.RIGHT'
title='Next location'
enabled={(-1) <= kindex && kindex + 1 < size}
- onClick={() => gotoIndex(kindex+1)}
+ onClick={() => gotoIndex(kindex + 1)}
/>
<Space />
<Label
@@ -218,11 +210,11 @@ export default function LocationsTable(): JSX.Element {
<Label className='locations' label={label} title={title} />
<Table
model={model}
- display={size >0}
+ display={size > 0}
selection={selected}
onSelection={(_row, _key, index) => gotoIndex(index)}
settings="ivette.locations.table"
- >
+ >
<Column
id='index' label='#' align='center' width={25}
render={renderIndex} />
diff --git a/ivette/src/frama-c/kernel/PivotTable.tsx b/ivette/src/frama-c/kernel/PivotTable.tsx
index 89fe885aaf6..fdf6b2c53e5 100644
--- a/ivette/src/frama-c/kernel/PivotTable.tsx
+++ b/ivette/src/frama-c/kernel/PivotTable.tsx
@@ -25,16 +25,19 @@
// --------------------------------------------------------------------------
import React from 'react';
-import { TitleBar } from 'ivette';
-import * as Server from 'frama-c/server';
import { Button } from 'dome/controls/buttons';
import { LED } from 'dome/controls/displays';
import { Scroll } from 'dome/layout/boxes';
-import * as Status from 'frama-c/kernel/Status';
-import * as States from 'frama-c/states';
import { GlobalState, useGlobalState } from 'dome/data/states';
+
+import { TitleBar } from 'ivette';
+import * as Display from 'ivette/display';
+
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
import * as PivotState from 'frama-c/plugins/pivot/api/general';
import PivotTableUI from 'react-pivottable/PivotTableUI';
+
import 'frama-c/kernel/PivotTable-style.css';
// --------------------------------------------------------------------------
@@ -78,10 +81,9 @@ function PivotTableBuild(): JSX.Element {
const [computing, setComputing] = React.useState(false);
const [error, setError] = React.useState('');
async function handleError(err: string): Promise<void> {
- const msg =
- `The pivot table could not be built: an error has occured (${err}).`;
- setError(msg);
- Status.setMessage({ text: msg, kind: 'error' });
+ const label = 'Pivot Table Error';
+ const title = `Building error (${err})`;
+ Display.showError({ label, title });
}
async function compute(): Promise<void> {
setComputing(true);
diff --git a/ivette/src/frama-c/kernel/Status.tsx b/ivette/src/frama-c/kernel/Status.tsx
deleted file mode 100644
index 5b1e0ff2761..00000000000
--- a/ivette/src/frama-c/kernel/Status.tsx
+++ /dev/null
@@ -1,97 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2023 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/* ************************************************************************ */
-
-/* --------------------------------------------------------------------------*/
-/* --- Frama-C Status Message ---*/
-/* --------------------------------------------------------------------------*/
-
-import _ from 'lodash';
-import React from 'react';
-import { Code, IconKind } from 'dome/controls/labels';
-import { IconButton } from 'dome/controls/buttons';
-import * as Toolbars from 'dome/frame/toolbars';
-import { GlobalState, useGlobalState } from 'dome/data/states';
-import * as Server from 'frama-c/server';
-
-export type kind =
- 'none' | 'info' | 'warning' | 'error' | 'success' | 'progress';
-
-export interface MessageProps {
- kind?: kind;
- text: string;
- title?: string;
-}
-
-const emptyMessage: MessageProps = { text: '', kind: 'none' };
-
-
-const GlobalMessage = new GlobalState(emptyMessage);
-
-const clearMessage = (): void => setMessage(emptyMessage);
-const triggerClearMessage = _.debounce(clearMessage, 15000);
-
-export function setMessage(message: MessageProps): void {
- GlobalMessage.setValue(message);
- triggerClearMessage();
-}
-
-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 { kind: mKind='none' } = message;
- const icon = msgIcon[mKind];
- const kind = msgKind[mKind];
- return (
- <Toolbars.Group display={message.kind !== 'none'} >
- <Code icon={icon} kind={kind}
- label={message.text} title={message.title} />
- <IconButton
- icon="CIRC.CLOSE"
- onClick={clearMessage}
- visible={message !== emptyMessage}
- title="Hide current message"
- />
- </Toolbars.Group>
- );
-}
-
-/* Callback on server events */
-
-{
- Server.onReady(() => setMessage(emptyMessage));
- Server.onShutdown(() => setMessage(emptyMessage));
-}
-
-/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/menu.ts b/ivette/src/frama-c/menu.ts
index b8dadcc57d8..bcb5ae8c7e5 100644
--- a/ivette/src/frama-c/menu.ts
+++ b/ivette/src/frama-c/menu.ts
@@ -24,14 +24,14 @@
/* --- Frama-C MENU ---*/
/* --------------------------------------------------------------------------*/
+import { ipcRenderer } from 'electron';
import * as Dome from 'dome';
import * as Dialogs from 'dome/dialogs';
+import * as Display from 'ivette/display';
import * as Server from 'frama-c/server';
import * as Services from 'frama-c/kernel/api/services';
import * as Ast from 'frama-c/kernel/api/ast';
-import * as Status from 'frama-c/kernel/Status';
import * as States from 'frama-c/states';
-import { ipcRenderer } from 'electron';
const cFilter = {
name: 'C source files',
@@ -43,10 +43,9 @@ const allFilter = {
};
async function parseFiles(files: string[]): Promise<void> {
- Status.setMessage({ text: 'Parsing source files…', kind: 'progress' });
await Server.send(Ast.setFiles, files);
await Server.send(Ast.compute, {});
- Status.setMessage({ text: 'Source files parsed.', kind: 'success' });
+ Display.showMessage('Source files parsed.');
return;
}
@@ -77,7 +76,6 @@ async function addFiles(): Promise<void> {
}
async function reparseFiles(): Promise<void> {
- Status.setMessage({ text: 'Parsing source files…', kind: 'progress' });
const files = await Server.send(Ast.getFiles, {});
if (files) {
await Server.send(Ast.setFiles, []);
@@ -88,15 +86,9 @@ async function reparseFiles(): Promise<void> {
async function loadSession(): Promise<void> {
const file = await Dialogs.showOpenFile({ title: 'Load a saved session' });
- Status.setMessage({ text: 'Loading session…', kind: 'progress' });
const error = await Server.send(Services.load, file);
States.clearHistory();
if (error) {
- Status.setMessage({
- text: 'Error when loading the session',
- title: error,
- kind: 'error',
- });
await Dialogs.showMessageBox({
message: 'An error has occurred when loading the file',
details: `File: ${file}\nError: ${error}`,
@@ -104,33 +96,20 @@ async function loadSession(): Promise<void> {
buttons: [{ label: 'Cancel' }],
});
}
- else
- Status.setMessage({
- text: 'Session successfully loaded.',
- kind: 'success',
- });
return;
}
async function saveSession(): Promise<void> {
const title = 'Save the current session';
const file = await Dialogs.showSaveFile({ title });
- Status.setMessage({ text: 'Saving session…', kind: 'progress' });
const error = await Server.send(Services.save, file);
if (error) {
- Status.setMessage({
- text: 'Error when saving the session',
- title: error,
- kind: 'error',
- });
await Dialogs.showMessageBox({
message: 'An error has occurred when saving the session',
kind: 'error',
buttons: [{ label: 'Cancel' }],
});
}
- else
- Status.setMessage({ text: 'Session successfully saved.', kind: 'success' });
return;
}
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index e802c9e01ab..20862aeedbd 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/ivette/src/frama-c/plugins/eva/valuetable.tsx
@@ -22,17 +22,17 @@
import React from 'react';
import _ from 'lodash';
-import * as Ivette from 'ivette';
import * as Dome from 'dome';
import * as System from 'dome/system';
+import { GlobalState, useGlobalState } from 'dome/data/states';
+import * as Ivette from 'ivette';
+import * as Display from 'ivette/display';
import * as States from 'frama-c/states';
import * as Server from 'frama-c/server';
-import * as Status from 'frama-c/kernel/Status';
import * as Ast from 'frama-c/kernel/api/ast';
import * as Eva from 'frama-c/plugins/eva/api/general';
import * as Values from 'frama-c/plugins/eva/api/values';
import EvaReady from './EvaReady';
-import { GlobalState, useGlobalState } from 'dome/data/states';
import { classes } from 'dome/misc/utils';
import { Icon } from 'dome/controls/icons';
@@ -921,7 +921,7 @@ interface EvaluationModeProps {
}
const evalShortcut = System.platform === 'macos' ? 'Cmd+E' : 'Ctrl+E';
-const evalMode : Ivette.SearchProps = {
+const evalMode: Ivette.SearchProps = {
id: 'frama-c.eva.evalMode',
label: 'Evaluation',
title: `Evaluate an ACSL expression (shortcut: ${evalShortcut})`,
@@ -951,13 +951,14 @@ function useEvaluationMode(props: EvaluationModeProps): void {
const onEnter = (pattern: string): void => {
const data = { stmt: marker, term: pattern };
const handleError = (err: string): void => {
- const text = `${pattern} could not be evaluated: ${err}.`;
- Status.setMessage({ text, kind: 'error' });
+ const label = 'Evaluation Error';
+ const title = `${pattern} could not be evaluated: ${err}.`;
+ Display.showWarning({ label, title });
};
const addProbe = (target: Ast.marker): void => {
setLocPin(scope, target, true);
- const text = `${pattern} evaluated in the 'Eva Values' panel`;
- Status.setMessage({ text, kind: 'success' });
+ Display.showMessage('New Probe');
+ Display.alertComponent('fc.eva.values');
};
Server.send(Ast.parseExpr, data).then(addProbe).catch(handleError);
};
diff --git a/ivette/src/frama-c/plugins/studia/index.ts b/ivette/src/frama-c/plugins/studia/index.ts
index 817a1779611..1cbbbf2dfd3 100644
--- a/ivette/src/frama-c/plugins/studia/index.ts
+++ b/ivette/src/frama-c/plugins/studia/index.ts
@@ -22,9 +22,9 @@
import * as Dome from 'dome';
import * as Ivette from 'ivette';
+import * as Display from 'ivette/display';
import * as States from 'frama-c/states';
import * as Server from 'frama-c/server';
-import * as Status from 'frama-c/kernel/Status';
import * as Ast from 'frama-c/kernel/api/ast';
import * as ASTview from 'frama-c/kernel/ASTview';
import * as Locations from 'frama-c/kernel/Locations';
@@ -34,8 +34,7 @@ import './style.css';
type access = 'Reads' | 'Writes';
function handleError(err: string): void {
- const text = `Studia failure: ${err}.`;
- Status.setMessage({ text, kind: 'error' });
+ Display.showWarning({ label: 'Studia Failure', title: `Error (${err})` });
}
async function computeStudiaSelection(
@@ -68,7 +67,7 @@ export function buildMenu(
attr: Ast.markerAttributesData,
): void {
const { marker, kind } = attr;
- switch(kind) {
+ switch (kind) {
case 'LVAL':
menu.push({
label: 'Studia: select reads of l-value',
@@ -108,7 +107,7 @@ export function buildMenu(
ASTview.registerMarkerMenuExtender(buildMenu);
-const studiaReadsMode : Ivette.SearchProps = {
+const studiaReadsMode: Ivette.SearchProps = {
id: 'frama-c.plugins.studia.reads',
rank: -1,
label: 'Studia: reads',
@@ -119,7 +118,7 @@ const studiaReadsMode : Ivette.SearchProps = {
onEnter: (p: string) => onEnter('Reads', p)
};
-const studiaWritesMode : Ivette.SearchProps = {
+const studiaWritesMode: Ivette.SearchProps = {
id: 'frama-c.plugins.studia.writes',
rank: -1,
label: 'Studia: writes',
diff --git a/ivette/src/ivette/display.tsx b/ivette/src/ivette/display.tsx
index 15d5f8ca4ae..962c21ad5b4 100644
--- a/ivette/src/ivette/display.tsx
+++ b/ivette/src/ivette/display.tsx
@@ -124,10 +124,12 @@ export function useComponentStatus(
return Laboratory.getComponentStatus(state, id ?? '');
}
-export type Message = undefined | null | string;
+export type ShortMessage = undefined | null | string;
+export type Message = ShortMessage | Laboratory.Notification;
+export type Warning = ShortMessage | { label: string, title: string };
/** Message notification */
-export function showMessage(msg: Message | Laboratory.Notification): void {
+export function showMessage(msg: Message): void {
if (!msg) return;
Laboratory.showMessage(typeof msg === 'string' ? { label: msg } : msg);
}
@@ -135,13 +137,19 @@ export function showMessage(msg: Message | Laboratory.Notification): void {
/** Warning notification. */
export function showWarning(msg: Message): void {
if (!msg) return;
- Laboratory.showMessage({ kind: 'warning', label: msg });
+ const short = typeof msg === 'string';
+ const label = short ? msg : msg.label;
+ const title = short ? msg : undefined;
+ Laboratory.showMessage({ kind: 'warning', label, title });
}
/** Error notification */
export function showError(msg: Message): void {
if (!msg) return;
- Laboratory.showMessage({ kind: 'error', label: msg });
+ const short = typeof msg === 'string';
+ const label = short ? msg : msg.label;
+ const title = short ? msg : undefined;
+ Laboratory.showMessage({ kind: 'error', label, title });
}
export function clearMessages(): void {
diff --git a/ivette/src/ivette/prefs.tsx b/ivette/src/ivette/prefs.tsx
index 5b5f3ae2229..dd7d28a7263 100644
--- a/ivette/src/ivette/prefs.tsx
+++ b/ivette/src/ivette/prefs.tsx
@@ -104,6 +104,6 @@ export const ConsoleScrollback =
// in seconds; 0 means no timeout
export const NotificationTimer =
- new Settings.GNumber('Laboratory.Notifications', 5);
+ new Settings.GNumber('Laboratory.Notifications', 10);
// --------------------------------------------------------------------------
--
GitLab