diff --git a/ivette/.gitignore b/ivette/.gitignore
index 7b638a52405ced0af29e48e3aa9f92eb13e27f01..194fc7ea7ce2c5c7ffb30e127542107772220cd0 100644
--- a/ivette/.gitignore
+++ b/ivette/.gitignore
@@ -5,7 +5,6 @@
.ivette
.dome-*.stamp
.dome-*.back
-.server-tsc
node_modules
yarn.lock
yarn-error.log
diff --git a/ivette/backup/sandbox/Project.js b/ivette/backup/sandbox/Project.js
deleted file mode 100644
index 37d33df468aedf4ad087430193c8e6ba1c18d445..0000000000000000000000000000000000000000
--- a/ivette/backup/sandbox/Project.js
+++ /dev/null
@@ -1,206 +0,0 @@
-import React, { useState, useEffect } from 'react';
-import { showOpenFiles } from 'dome/dialogs';
-import { Button } from 'dome/controls/buttons';
-import { Label } from 'dome/controls/labels';
-import { Badge } from 'dome/controls/icons';
-import { Hbox, Vbox } from 'dome/layout/boxes';
-import Server from './server';
-import { Set } from 'immutable';
-
-class SelectList extends React.Component {
- render() {
- return (
- <select value={this.props.value} onChange={this.props.onChange}>
- {this.props.values.map(v => <option key={v.id}>{v.name}</option>)}
- </select>
- )
- }
-}
-
-function FileSelect(props) {
- const [files, setFiles] = useState(Set([]));
- const [addedFiles, setAddedFiles] = useState(Set([]));
- const [removedFiles, setRemovedFiles] = useState(Set([]));
-
- function updateFiles() {
- Server
- .sendGET("kernel.ast.getFiles", [], false)
- .then(
- (data) => {
- console.log("success: " + data + '\n');
- setFiles(Set(data));
- setAddedFiles(Set([]));
- setRemovedFiles(Set([]));
- },
- (_rid, data) => {
- console.log("err:" + data + '\n')
- });
- };
-
- //Done only once
- useEffect(updateFiles, []);
-
- function addFiles() {
- showOpenFiles({ message: "Add files" })
- .then(files => {
- setAddedFiles(() => {
- const sfiles = Set(files);
- const res = addedFiles.union(sfiles);
- return res
- })
- });
- };
-
- function generateItem(v) {
- const removed = removedFiles.has(v);
- const added = addedFiles.has(v);
- return (
- <Hbox key={v}>
- <Label
- style={(removed ? { color: 'red' } : (added ? { color: 'green' } : {}))}>
- {v}
- </Label>
- <Badge
- value={removed ? 'CIRC.PLUS' : 'CIRC.MINUS'}
- onClick={() =>
- setRemovedFiles(() =>
- removed ? removedFiles.remove(v) : removedFiles.add(v))
- } />
- </Hbox>
- )
- };
-
- function sendFiles() {
- const filesToSend = files.union(addedFiles).subtract(removedFiles);
- Server
- .sendSET("kernel.ast.setFiles", filesToSend.toArray(), false)
- .then(
- () => {
- console.log("setFiles: success");
- Server
- .sendEXEC("kernel.ast.execCompute", [], false)
- .then(
- () => {
- console.log("execComput: success");
- updateFiles();
- },
- (_rid, data) => {
- console.log("execCompute err:" + data + '\n')
- }
- );
- },
- (_rid, data) => {
- console.log("setFiles err:" + data + '\n')
- }
- );
- };
-
- return (
- <Vbox>
- {files.map(generateItem)}
- {addedFiles.map(generateItem)}
- <Hbox>
- <Button label='Add files' onClick={addFiles} />
- <Button label='Update' onClick={sendFiles} />
- </Hbox>
- </Vbox>
- )
-}
-
-function Projects(props) {
- const [projects, setProjects] = useState([]);
- const [current, setCurrent] = useState(undefined);
- const [newName, setNewName] = useState("project_name");
-
-
- function updateProjects() {
- Server
- .sendGET("kernel.project.getList", [], false)
- .then(
- (data) => {
- console.log("success: " + data.datadir + '\n');
- setProjects(data)
- },
- (_rid, data) => {
- console.log("err:" + data + '\n')
- });
- };
-
- //Done only once
- useEffect(updateProjects, []);
-
- function new_project() {
- Server
- .sendSET("kernel.project.setCreate", newName, false)
- .then(
- (data) => {
- console.log("success: " + data.datadir + '\n');
- updateProjects();
- },
- (_rid, data) => {
- console.log("err:" + data + '\n')
- });
- };
-
-
- console.log("projects:", projects);
- return (
- <Hbox>
- <form onSubmit={new_project}>
- <label>
- Name of new project :
- <input
- type="text"
- value={newName}
- onChange={event => setNewName(event.target.value)}
- />
- </label>
- <input type="submit" value="Create" />
- </form>
- <label>
- Current project:
- <SelectList
- values={projects}
- value={current}
- onChange={event => setCurrent(event.target.value)}
- />
- </label>
- </Hbox>
- )
-}
-
-function Kernel(props) {
- const [state, setState] = useState("undefined");
-
- function getCfg() {
- console.log("send request\n");
- Server
- .sendGET("kernel.getConfig", [], false)
- .then(
- (data) => {
- console.log("success: " + data.datadir + '\n');
- setState(data.datadir);
- },
- (_rid, data) => {
- console.log("err:" + data + '\n')
- });
- };
-
- return (
- <Hbox>
- <Button label='GetConfig' onClick={getCfg} />
- <Label label={state} />
- </Hbox>
- )
-}
-
-export default function Project(props) {
-
- return (
- <>
- <Kernel />
- <Projects />
- <FileSelect />
- </>
- )
-}
\ No newline at end of file
diff --git a/ivette/backup/sandbox/Properties.js b/ivette/backup/sandbox/Properties.js
deleted file mode 100644
index ac8e770bef928215afea13c5dc33985af090daf4..0000000000000000000000000000000000000000
--- a/ivette/backup/sandbox/Properties.js
+++ /dev/null
@@ -1,137 +0,0 @@
-// --------------------------------------------------------------------------
-// --- Frama-C Properties Table
-// --------------------------------------------------------------------------
-
-import React from 'react' ;
-import Dome from 'dome' ;
-import { useState, useEffect } from 'react' ;
-
-import { Button } from 'dome/controls/buttons';
-import { Vfill, Vbox, Scroll } from 'dome/layout/boxes' ;
-import { Splitter } from 'dome/layout/splitters' ;
-import { Column, Table } from 'dome/table/views' ;
-import { ArrayModel } from 'dome/table/arrays' ;
-import { Form, Section, FieldList, FieldCheckbox, FieldRadio } from 'dome/layout/forms' ;
-
-import Server from './server.js' ;
-import Events from './Events.js' ;
-
-export default function Properties (props) {
- const model = props.properties;
-
- /* --- Columns of the table ----------------------------------------------- */
-
- const columnFile = <Column id='file'
- label='File' />;
- const columnFct = <Column id='fct'
- label='Function' />;
- const columnProp = <Column id='property'
- label='Property'
- fill />;
- const columnStatus = <Column id='status'
- label='Status' />;
-
- /* The default columns displayed. The property column is always shown. */
- const defaultColumns =
- { path:false,
- fct:true,
- status:true,
- };
- /* The columns displayed. Set by the user through a form. */
- const [columnsValue, _] = useState(defaultColumns);
-
- /* Builds the array of columns according to [columnsValue]. */
- function makeColumns () {
- const columns = new Array();
- if (columnsValue.path)
- columns.push(columnFile);
- if (columnsValue.fct)
- columns.push(columnFct);
- columns.push(columnProp); // Always shown.
- if (columnsValue.status)
- columns.push(columnStatus);
- return columns;
- }
-
- /* The columns array used by the table. */
- const [ columns, setColumns ] = useState(makeColumns());
-
- function onChangeColumns () {
- setColumns(makeColumns());
- }
-
- /* Form to choose the columns displayed. */
- const columns_list =
- <Form value={columnsValue} onChange={onChangeColumns} >
- <Section label="Columns" unfold='false' >
- <FieldCheckbox label="File" path='path' />
- <FieldCheckbox label="Function" path='fct' />
- <FieldCheckbox label="Status" path='status' />
- </Section>
- </Form>;
-
- /* --- Filters of logical properties ------------------------------------- */
-
- /* All properties are shown by default. */
- const default_status =
- { valid:true,
- valid_hyp:true,
- unknown:true,
- invalid:true,
- invalid_hyp:true,
- considered_valid:true,
- untried:true,
- dead:true,
- inconsistent:true
- };
- const [status, setStatus] = useState(default_status);
-
- /* Function filtering the properties by status. */
- function filter (item) {
- switch (item.status) {
- case 'Valid':
- case 'Valid_but_dead': return status.valid;
- case 'Valid_under_hyp': return status.valid_hyp;
- case 'Invalid':
- case 'Invalid_but_dead': return status.invalid;
- case 'Invalid_under_hyp': return status.invalid_hyp;
- case 'Unknown':
- case 'Unknown_but_dead': return status.unknown;
- case 'Considered_valid': return status.considered_valid;
- case 'Never_tried': return status.untried;
- case 'Dead': return status.dead;
- case 'Inconsistent': return status.inconsistent;
- default: return true;
- }
- }
-
- function onChangeFilter (value, error) {
- model.setFiltering(filter);
- }
-
- /* Filters selection. */
- const filter_list =
- <Form value={status} onChange={onChangeFilter} >
- <Section label="Status" unfold='true' >
- <FieldCheckbox label="Valid" path='valid' />
- <FieldCheckbox label="Valid under hyp." path='valid_hyp' />
- <FieldCheckbox label="Unknown" path='unknown' />
- <FieldCheckbox label="Invalid" path='invalid' />
- <FieldCheckbox label="Invalid under hyp." path='invalid_hyp' />
- <FieldCheckbox label="Considered valid" path='considered_valid' />
- <FieldCheckbox label="Untried" path='untried' />
- <FieldCheckbox label="Dead" path='dead' />
- <FieldCheckbox label="Inconsistent" path='inconsistent' />
- </Section>
- </Form>;
-
- /* Table of logical properties. */
- const table = <Table model={model} children={columns} />;
-
- return (
- <Splitter dir='LEFT' >
- <Vfill> <Scroll> {filter_list} {columns_list} </Scroll> </Vfill>
- <Vfill> {table} </Vfill>
- </Splitter>
- )
-}
diff --git a/ivette/backup/sandbox/SourceCode.js b/ivette/backup/sandbox/SourceCode.js
deleted file mode 100644
index 023eeafbfb30a162fb9aebacb2217358969aec90..0000000000000000000000000000000000000000
--- a/ivette/backup/sandbox/SourceCode.js
+++ /dev/null
@@ -1,129 +0,0 @@
-// --------------------------------------------------------------------------
-// --- Frama-C Source Panel
-// -------------------------------------------------------------------------
-
-import React from 'react' ;
-import Dome from 'dome' ;
-
-import { Button } from 'dome/controls/buttons';
-import Toolbar from 'dome/layout/toolbars' ;
-import { Hbox, Hfill, Vbox, Vfill, Space } from 'dome/layout/boxes' ;
-import { Splitter } from 'dome/layout/splitters' ;
-import { Column, Table } from 'dome/table/views' ;
-import { Text } from 'dome/text/editors' ;
-import Server from './server.js' ;
-import Events from './Events.js' ;
-
-import { useState, useEffect } from 'react' ;
-
-import 'codemirror/mode/clike/clike.js';
-import 'codemirror/theme/ambiance.css' ;
-import 'codemirror/theme/solarized.css';
-
-/* Pretty prints the source code from [text] in [buffer]. */
-function printSource (buffer, text) {
- if (text === null) return;
- if (Array.isArray(text)) {
- const tag = text.shift();
- if (tag !== '') {
- buffer.openTextMarker( { id:tag } );
- text.forEach(txt => printSource(buffer, txt));
- buffer.closeTextMarker();
- } else
- text.forEach(txt => printSource(buffer, txt));
- } else
- buffer.append(text);
-}
-
-/* Display the list of functions and the source code for the selected function
- in the list. */
-export default function Source (props) {
- /* Buffer for the source code. */
- const buffer = props.sourceCode;
- /* Model for the function list. */
- const model = props.functions;
-
- /* Print the source code of the function [data.fct]. */
- function printFunction (data) {
- console.log("Select function: " + data.fct);
- Server.sendGET("kernel.ast.printFunction", data.fct, false).then
- ( data => {
- buffer.clear();
- printSource(buffer, data);
- });
- }
-
- const [ theme, setTheme ] = useState('default');
- function selectTheme (name) {
- return function () { setTheme(name); }
- }
-
- function contextMenu (data) {
- const item1 = { label:"Default", onClick:selectTheme("default") };
- const item2 = { label:"Ambiance", onClick:selectTheme("ambiance") };
- const item3 = { label:"Solarized light", onClick:selectTheme("solarized light") };
- const item4 = { label:"Solarized dark", onClick:selectTheme("solarized dark") };
- Dome.popupMenu([item1, item2, item3, item4]).catch(() => {});
- }
-
- /* Table for the function list. */
- const table =
- <Table model={model}
- onSelection={printFunction} >
- <Column id='fct'
- label='Functions'
- title='List of functions in the current Frama-C project' />
- </Table>;
-
- const [ lineWrapping, setLineWrapping ] = useState(false);
- function changeLineWrapping () { setLineWrapping(!lineWrapping); }
-
- const code = <Text buffer={buffer}
- mode='text/x-csrc'
- theme={theme}
- lineWrapping={lineWrapping}
- readOnly />;
-
- const [ fontSize, setFontSize ] = useState(12);
- function increaseFontSize () { setFontSize(fontSize + 2); }
- function decreaseFontSize () { setFontSize(fontSize - 2); }
-
- const toolbar =
- <Toolbar.ToolBar>
- <Toolbar.Space/>
- <Toolbar.Select
- value={theme}
- onChange={(name) => {selectTheme(name)();}} >
- <option value='default' label='Default'/>
- <option value='ambiance' label='Ambiance'/>
- <option value='solarized light' label='Solarized light'/>
- <option value='solarized dark' label='Solarized dark'/>
- </Toolbar.Select>
- <Toolbar.ButtonGroup>
- <Toolbar.Button
- icon='MINUS'
- title='Decrease the font size'
- onClick={decreaseFontSize}
- />
- <Toolbar.Button
- icon='PLUS'
- title='Increase the font size'
- onClick={increaseFontSize}
- />
- </Toolbar.ButtonGroup>
- <Toolbar.Button icon={lineWrapping ? "CHECK" : "CROSS"}
- label="Line wrapping"
- title="Change line wrapping mode"
- onClick={changeLineWrapping} />
- </Toolbar.ToolBar>;
-
- return (
- <Splitter dir='LEFT' >
- <Vfill style={{ minWidth: 100 }}> {table} </Vfill>
- <Vfill onContextMenu={contextMenu} style={{ fontSize: fontSize }} >
- {toolbar}
- {code}
- </Vfill>
- </Splitter>
- );
-}
diff --git a/ivette/backup/sandbox/SourceFiles.js b/ivette/backup/sandbox/SourceFiles.js
deleted file mode 100644
index 8a7386b57064bb60670ecca9b6145651e6b236c5..0000000000000000000000000000000000000000
--- a/ivette/backup/sandbox/SourceFiles.js
+++ /dev/null
@@ -1,44 +0,0 @@
-import React, { useState, useEffect } from 'react';
-import { Buffer } from 'dome/text/buffers'
-import { Text } from 'dome/text/editors';
-import Server from './server';
-import System from 'dome/system';
-import 'codemirror/mode/clike/clike.js';
-
-export default function SourceFiles() {
-
- const [filenames, setFilenames] = useState([]);
- const buffer = new Buffer({ mode: 'text/x-csrc' });
-
- function getSourceFilenames() {
- console.log('SourceFiles::getFiles');
-
- Server
- .sendGET("kernel.ast.getFiles", [], false)
- .then(
- (fnames) => {
- console.log('Got source filenames:' + fnames);
- setFilenames(fnames);
- });
- }
-
- useEffect(getSourceFilenames, []);
-
- useEffect(() => {
- if (filenames.length > 0) {
- console.log('Displaying ' + filenames[0] + '!');
- System
- .readFile(filenames[0])
- .then(
- (fcontent) => {
- console.log('Got file content: ' + fcontent);
- buffer.clear();
- buffer.append(fcontent);
- });
- }
- }, [filenames])
-
- return (
- <Text buffer={buffer} readOnly='true' lineNumbers='true' />
- )
-}
diff --git a/ivette/src/dome/src/renderer/data/json.ts b/ivette/src/dome/src/renderer/data/json.ts
index 018fe14b19477769249dd41d4e2b24d0cb0bf870..195aec66a84ce337ea88226f72ec6eda57213713 100644
--- a/ivette/src/dome/src/renderer/data/json.ts
+++ b/ivette/src/dome/src/renderer/data/json.ts
@@ -123,8 +123,7 @@ export function jEnum<A>(d: { [tag: string]: A }): Loose<A> {
/**
One of the enumerated _constants_ or `undefined`.
The typechecker will prevent you from listing values that are not in
- type `A`. However, it will not protected you
- from missings constants in `A`.
+ type `A`. However, it will not protected you from missings constants in `A`.
*/
export function jTags<A>(...values: ((string | number) & A)[]): Loose<A> {
var m = new Map<string | number, A>();