diff --git a/ivette/.eslintrc.js b/ivette/.eslintrc.js
index e57c8f64dbc20e9ed697cf0cf85f6090a5b84a41..163e36aee57deb7cfda15a74345bb71c0f2eb006 100644
--- a/ivette/.eslintrc.js
+++ b/ivette/.eslintrc.js
@@ -51,6 +51,8 @@ module.exports = {
"padded-blocks": "off",
// Allow braces on their own line
"@typescript-eslint/brace-style": "off",
+ // Allow range conditions such as 0 <= x && x < 10
+ "yoda": [2, "never", { "onlyEquality": true }],
// Allow single command on new line after 'if' statement
"curly": "off",
// Do not specify position for single commands
diff --git a/ivette/src/dome/src/renderer/controls/buttons.js b/ivette/src/dome/src/renderer/controls/buttons.js
index c1bb0d0724d4b633e58c6967929ffc5e920a3512..fcb2709e94abcff9ca8ff2bb4ff377d3abb32054 100644
--- a/ivette/src/dome/src/renderer/controls/buttons.js
+++ b/ivette/src/dome/src/renderer/controls/buttons.js
@@ -118,7 +118,7 @@ const LABEL = ({disabled,label}) => (
Buttons without focus can not be triggered with the Enter key.
*/
export const Button = (props) => {
- const disabled = DISABLED(props);
+ const disabled = props.onClick ? DISABLED(props) : true ;
const { focusable=false, kind='default',
visible=true, display=true, blink=false,
selected, icon, label, className='' } = props;
@@ -176,7 +176,7 @@ export const Button = (props) => {
Buttons without focus can not be triggered with the Enter key.
*/
export const CircButton = (props) => {
- const disabled = DISABLED(props);
+ const disabled = props.onClick ? DISABLED(props) : true ;
const { focusable=false, kind='default',
visible=true, display=true,
selected, icon, label, className='' } = props;
@@ -229,7 +229,7 @@ export const CircButton = (props) => {
- `'negative'`: negative button, in red.
*/
export const IconButton = (props) => {
- const disabled = DISABLED(props);
+ const disabled = props.onClick ? DISABLED(props) : true;
const {
icon, size, title,
visible=true, display=true, selected,
@@ -271,7 +271,7 @@ const CHECKBOX_DISABLED = 'dome-control-disabled dome-xCheckbox ' ;
@property {object} [style] - Additional style
*/
export const Checkbox = (props) => {
- const disabled = DISABLED(props);
+ const disabled = onChange ? DISABLED(props) : true;
const onChange = props.onChange && ((evt) => props.onChange(evt.target.checked)) ;
const baseClass = disabled ? CHECKBOX_DISABLED : CHECKBOX_ENABLED ;
const labelClass = props.className || '' ;
@@ -307,12 +307,11 @@ export const Checkbox = (props) => {
@property {object} [style] - Additional style
*/
export const Switch = (props) => {
- const disabled = DISABLED(props);
+ const disabled = props.onChange ? DISABLED(props) : undefined ;
const { visible=true, display=true } = props ;
const onChange = props.onChange && ((evt) => props.onChange(evt.target.checked)) ;
const iconId = props.value ? 'SWITCH.ON' : 'SWITCH.OFF' ;
- const onClick = (disabled || !props.onChange)
- ? undefined : () => props.onChange(!props.value) ;
+ const onClick = disabled ? undefined : () => props.onChange(!props.value) ;
const className = 'dome-xSwitch '
+ (disabled ? 'dome-control-disabled' : 'dome-control-enabled')
+ (visible ? '' : ' dome-control-hidden')
@@ -353,7 +352,7 @@ export const Switch = (props) => {
with HTML standards and DOM element properties.
*/
export const Radio = (props) => {
- const disabled = DISABLED(props);
+ const disabled = props.onSelection ? DISABLED(props) : true;
const checked = props.value === props.selection ;
const onChange = props.onSelection && (() => props.onSelection(props.value)) ;
const baseClass = disabled ? CHECKBOX_DISABLED : CHECKBOX_ENABLED ;
@@ -363,7 +362,8 @@ export const Radio = (props) => {
title={props.title}
style={props.style}
className={baseClass + labelClass} >
- <input type="radio" disabled={disabled} checked={checked} onChange={onChange} />
+ <input type="radio"
+ disabled={disabled} checked={checked} onChange={onChange} />
{props.label}
</label>
);
@@ -415,8 +415,9 @@ export class RadioGroup extends React.Component {
}
render() {
- const groupdisabled = DISABLED(this.props);
- const { className='', style } = this.props ;
+ const props = this.props ;
+ const groupdisabled = props.onChange ? DISABLED(props) : true ;
+ const { className='', style } = props ;
const selection = this.state.value ;
const makeRadio = (radio) => {
const disabled = groupdisabled || DISABLED(radio.props) ;
@@ -424,7 +425,7 @@ export class RadioGroup extends React.Component {
const onSelection =
onRadioSelect
? (v) => { onRadioSelect(v) ; this.onChange(v); }
- : this.handleSelect ;
+ : this.onChange ;
return React.cloneElement( radio , { selection , disabled , onSelection } , null );
} ;
return (
diff --git a/ivette/src/dome/src/renderer/controls/icons.json b/ivette/src/dome/src/renderer/controls/icons.json
index 681bb6d5286a132d76594580042d864e12cec557..dbe695a6bcb167ef5bf1b97b004d2df3888477b1 100644
--- a/ivette/src/dome/src/renderer/controls/icons.json
+++ b/ivette/src/dome/src/renderer/controls/icons.json
@@ -35,6 +35,12 @@
"viewBox": "0 0 26 24",
"path": "M8.263 18.737l-0.67 0.67q-0.134 0.134-0.308 0.134t-0.308-0.134l-6.241-6.241q-0.134-0.134-0.134-0.308t0.134-0.308l6.241-6.241q0.134-0.134 0.308-0.134t0.308 0.134l0.67 0.67q0.134 0.134 0.134 0.308t-0.134 0.308l-5.263 5.263 5.263 5.263q0.134 0.134 0.134 0.308t-0.134 0.308zM16.179 4.446l-4.996 17.29q-0.054 0.174-0.208 0.261t-0.315 0.033l-0.83-0.228q-0.174-0.054-0.261-0.208t-0.033-0.328l4.996-17.29q0.054-0.174 0.208-0.261t0.315-0.033l0.83 0.228q0.174 0.054 0.261 0.208t0.033 0.328zM24.978 13.165l-6.241 6.241q-0.134 0.134-0.308 0.134t-0.308-0.134l-0.67-0.67q-0.134-0.134-0.134-0.308t0.134-0.308l5.263-5.263-5.263-5.263q-0.134-0.134-0.134-0.308t0.134-0.308l0.67-0.67q0.134-0.134 0.308-0.134t0.308 0.134l6.241 6.241q0.134 0.134 0.134 0.308t-0.134 0.308z"
},
+ "TERMINAL": {
+ "section": "Tools",
+ "title": "Terminal",
+ "viewBox": "0 0 15 16",
+ "path": "M5.223 8.777l-4.161 4.161q-0.089 0.089-0.205 0.089t-0.205-0.089l-0.446-0.446q-0.089-0.089-0.089-0.205t0.089-0.205l3.509-3.509-3.509-3.509q-0.089-0.089-0.089-0.205t0.089-0.205l0.446-0.446q0.089-0.089 0.205-0.089t0.205 0.089l4.161 4.161q0.089 0.089 0.089 0.205t-0.089 0.205zM14.857 12.857v0.571q0 0.125-0.080 0.205t-0.205 0.080h-8.571q-0.125 0-0.205-0.080t-0.080-0.205v-0.571q0-0.125 0.080-0.205t0.205-0.080h8.571q0.125 0 0.205 0.080t0.080 0.205z"
+ },
"EXECUTE": {
"section": "Tools",
"viewBox": "0 0 16 16",
diff --git a/ivette/src/dome/src/renderer/dome.js b/ivette/src/dome/src/renderer/dome.js
index 81de82545f3b09c424f98fb8c1b1710362bbf3e1..8dbe53f7deaa69d480c2903332fbfe695e10bf64 100644
--- a/ivette/src/dome/src/renderer/dome.js
+++ b/ivette/src/dome/src/renderer/dome.js
@@ -738,74 +738,6 @@ export function useSwitch( settings, defaultValue=false )
return [ value, v => update(v===undefined ? !value : v) ];
}
-/**
- @summary Local state for managing history.
- @param {string} [settings] - global window settings to store the history
- @param {any} [defaultValue] - default current value
- @return {object} for managing the history
- @description
-The returned object contains the following properties:
-
-- `current` the current value in the history
-- `prev:()=>value` optional function for shifting to the next item (if any)
-- `next:()=>value` optional function for shifting to the previous item (if any)
-- `length:number` history size
-- `index:number` position in the history (starting from `0`)
-- `insert:(v)=>value` insert value `v` as the new current value
-- `fork:(v)=>value` insert value `v` but clear next items (if any)
-- `add:(v)=>value` insert value `v` in front of the history
-- `update:(v)=>value` only change the current value
-- `clear:()=>void` clear the history
-
-When inserting a value, previous and current values are kept in the history.
-When updating or insering a falsy value, the history is shifted to the next
-or previous element available in the history. You can drop the current value from the history
-with `update(undefined)`.
-All updating functions return the new current value.
-*/
-
-export function useHistory( settings, defaultValue )
-{
- const [ { next,prev,current } , setHistory ] =
- useSettings( true, settings, { next:[], prev:[], current:defaultValue } );
- const setState = ({ next, prev, current }) => {
- while( !current && next.length ) current = next.shift();
- while( !current && prev.length ) current = prev.shift();
- setHistory({next: next.slice(), prev: prev.slice(), current });
- return current ;
- };
- const insert = (v) => {
- if (current) prev.unshift(current);
- return setState({ next, prev, current:v });
- };
- const fork = (v) => {
- if (current) prev.unshift(current);
- return setState({ next:[], prev, current:v });
- };
- const append = (v) => {
- return setState({next:[], prev: next.reverse().append(current || [],next), current:v });
- };
- const move = ( src , tgt ) => src.length ? (() => {
- let v = src.shift();
- if (current) tgt.unshift(current);
- return setState({ current:v, prev, next });
- }) : undefined;
- const update = (v) => setState({ next, prev, current:v });
- const clear = (next.length || prev.length || current) && (() => setState({ next:[], prev:[] }));
- return {
- length:next.length + prev.length + (current ? 1 : 0),
- index:next.length,
- current,
- insert,
- fork,
- append,
- update,
- next:move(next,prev),
- prev:move(prev,next),
- clear
- };
-}
-
/**
@summary Local state with global settings (Custom React Hook).
@param {string} settings - global settings for storing the value
diff --git a/ivette/src/dome/src/renderer/text/buffers.js b/ivette/src/dome/src/renderer/text/buffers.js
index bf6a2f190b7cef9f13fcb453838b51250dcfaed0..30c272d3f99a511b7d3b98b31320ac37bd418b8d 100644
--- a/ivette/src/dome/src/renderer/text/buffers.js
+++ b/ivette/src/dome/src/renderer/text/buffers.js
@@ -95,9 +95,12 @@ export class RichTextBuffer extends Emitter {
this.setFocused = this.setFocused.bind(this);
this.clear = this.clear.bind(this);
this.append = this.append.bind(this);
+ this.setValue = this.setValue.bind(this);
+ this.getValue = this.getValue.bind(this);
this.log = this.log.bind(this);
this._doc.on('change', ( _target , { origin } ) => {
if (origin !== 'buffer') this.setEdited(true);
+ this.emit('change');
});
}
@@ -119,14 +122,7 @@ export class RichTextBuffer extends Emitter {
// --------------------------------------------------------------------------
/** Clear buffer contents and resets _edited_ state. */
- clear() {
- this._doc.setValue('');
- this._edited = false;
- this._stacked = [] ;
- this._focused = false ;
- this._markid = 0 ;
- this._markers = {} ;
- }
+ clear() { this.setValue(''); }
/**
@summary Writes in the buffer.
@@ -171,6 +167,27 @@ export class RichTextBuffer extends Emitter {
this.scroll();
}
+ /**
+ @summary Replace textual content with the given value.
+ @param {string} [txt] - new text content
+ @description
+ Also remove all markers.
+ */
+ setValue(txt='') {
+ this._doc.setValue(txt);
+ this._edited = false;
+ this._stacked = [] ;
+ this._focused = false ;
+ this._markid = 0 ;
+ this._markers = {} ;
+ }
+
+ /**
+ @summary Return textual content.
+ @return {string}
+ */
+ getValue() { return this._doc.getValue(); }
+
/**
@summary Opens a text marker.
@param {object} options - CodeMirror
diff --git a/ivette/src/frama-c/style.css b/ivette/src/frama-c/style.css
index f918358dc93d2336f9dc83ae63778c1913374f26..79a3307a70214e7304248a083e1ae2f724f90f34 100644
--- a/ivette/src/frama-c/style.css
+++ b/ivette/src/frama-c/style.css
@@ -37,11 +37,6 @@
height: 24px ;
}
-.labview-titlebar .dome-xLabel
-{
- padding-top: 4px ;
-}
-
.labview-handle
{
flex: 1 1 auto ;
diff --git a/ivette/src/renderer/Controller.tsx b/ivette/src/renderer/Controller.tsx
index 60387fdd6c8e15333575e7cf1855d879a70a1036..d463bdbac3b9829a3dfef68c950f8e0d40a912d6 100644
--- a/ivette/src/renderer/Controller.tsx
+++ b/ivette/src/renderer/Controller.tsx
@@ -20,32 +20,31 @@ import 'codemirror/theme/ambiance.css';
// --- Configure Server
// --------------------------------------------------------------------------
-let cmdConfig: Server.Configuration;
-const cmdLine = new RichTextBuffer();
+const quoteRe = new RegExp('^[-./:a-zA-Z0-9]+$');
+const quote = (s: string) => (quoteRe.test(s) ? s : `"${s}"`);
-function dumpCmdLine(sc: Server.Configuration): void {
+function dumpServerConfig(sc: Server.Configuration): string {
+ let buffer = '';
const { cwd, command, sockaddr, params } = sc;
- cmdLine.clear();
- if (cwd) cmdLine.log('--cwd', cwd);
- if (command) cmdLine.log('--command', command);
- if (sockaddr) cmdLine.log('--socket', sockaddr);
+ if (cwd) buffer += `--cwd ${quote(cwd)}\n`;
+ if (command) buffer += `--command ${command}\n`;
+ if (sockaddr) buffer += `--socket ${sockaddr}\n`;
if (params) {
params.forEach((v: string, i: number) => {
if (i > 0) {
if (v.startsWith('-') || v.endsWith('.c')
|| v.endsWith('.h') || v.endsWith('.i')) {
- cmdLine.append('\n');
- } else {
- cmdLine.append(' ');
- }
+ buffer += '\n';
+ } else
+ buffer += ' ';
}
- cmdLine.append(v);
+ buffer += v;
});
}
- cmdLine.append('\n');
+ return buffer;
}
-function buildServerConfiguration(argv: string[], cwd?: string) {
+function buildServerConfig(argv: string[], cwd?: string) {
const params = [];
let command;
let sockaddr;
@@ -77,10 +76,23 @@ function buildServerConfiguration(argv: string[], cwd?: string) {
};
}
+function insertConfig(hs: string[], cfg: Server.Configuration) {
+ const cmd = dumpServerConfig(cfg).trim();
+ const newhs =
+ hs.map((h) => h.trim())
+ .filter((h: string) => h !== cmd && h !== '')
+ .slice(0, 50);
+ newhs.unshift(cmd);
+ return newhs;
+}
+
+// --------------------------------------------------------------------------
+// --- Start Server on Command
+// --------------------------------------------------------------------------
+
Dome.onCommand((argv: string[], cwd: string) => {
- cmdConfig = buildServerConfiguration(argv, cwd);
- dumpCmdLine(cmdConfig);
- Server.configure(cmdConfig);
+ const cfg = buildServerConfig(argv, cwd);
+ Server.configure(cfg);
Server.start();
});
@@ -136,99 +148,146 @@ export const Control = () => {
// --- Server Console
// --------------------------------------------------------------------------
-function getCmdLine() {
- return cmdLine.getDoc().getValue().trim();
-}
-
-function execCmdLine(cmd: string) {
- const argv = cmd.split(/[ \t\n]+/);
- const cfg = buildServerConfiguration(argv);
- Server.configure(cfg);
- Server.restart();
-}
+const editor = new RichTextBuffer();
const RenderConsole = () => {
- const [command, switchCmd] = Dome.useSwitch();
- const { current, next, prev, index, length, update, insert, clear }: any =
- Dome.useHistory('frama-c.command.history');
+ const scratch = React.useRef([] as string[]);
+ const [cursor, setCursor] = React.useState(-1);
+ const [H0, setH0] = Dome.useState('Controller.history', []);
+ const [isEmpty, setEmpty] = React.useState(true);
+ const [noTrash, setNoTrash] = React.useState(true);
+
+ // Cope with merge settings that keeps previous array entries (BUG in DOME)
+ const history = Array.isArray(H0) ? H0.filter((h) => h !== '') : [];
+ const setHistory = (hs: string[]) => {
+ const n = hs.length;
+ setH0(n < 50 ? hs.concat(Array(50 - n).fill('')) : hs);
+ };
+
+ Dome.useEmitter(editor, 'change', () => {
+ const cmd = editor.getValue().trim();
+ setEmpty(cmd === '');
+ setNoTrash(cursor === 0 && history.length === 1 && cmd === history[0]);
+ });
+
+ const doReload = () => {
+ const cfg = Server.getConfig();
+ const hst = insertConfig(history, cfg);
+ scratch.current = hst.slice();
+ editor.setValue(hst[0]);
+ setHistory(hst);
+ setCursor(0);
+ };
+
+ const doSwitch = () => {
+ if (cursor < 0) doReload();
+ else {
+ editor.clear();
+ scratch.current = [];
+ setCursor(-1);
+ }
+ };
const doExec = () => {
- const cmdline = getCmdLine();
- if (cmdline !== current) insert(cmdline);
- execCmdLine(cmdline);
- switchCmd();
+ const cmd = editor.getValue().trim();
+ const argv = cmd.split(/[ \t\n]+/);
+ const cfg = buildServerConfig(argv);
+ const hst = insertConfig(history, cfg);
+ setHistory(hst);
+ setCursor(-1);
+ editor.clear();
+ Server.configure(cfg);
+ Server.restart();
+ };
+
+ const doMove = (target: number) => {
+ if (0 <= target && target < history.length && target !== cursor)
+ return () => {
+ const cmd = editor.getValue();
+ const pad = scratch.current;
+ pad[cursor] = cmd;
+ editor.setValue(pad[target]);
+ setCursor(target);
+ };
+ return undefined;
};
- const doNext = () => { cmdLine.getDoc().setValue(next() || ''); };
- const doPrev = () => { cmdLine.getDoc().setValue(prev() || ''); };
- const doReload = () => { dumpCmdLine(cmdConfig); };
- const doDrop = () => {
- cmdLine.clear();
- cmdLine.getDoc().setValue(update(undefined) || '');
+
+ const doRemove = () => {
+ const n = history.length;
+ if (n <= 1) doReload();
+ else {
+ const hst = history.slice();
+ const pad = scratch.current;
+ hst.splice(cursor, 1);
+ pad.splice(cursor, 1);
+ setHistory(hst);
+ const next = cursor > 0 ? cursor - 1 : 0;
+ editor.setValue(pad[next]);
+ setCursor(next);
+ }
};
+
+ const doPrev = doMove(cursor + 1);
+ const doNext = doMove(cursor - 1);
+ const edited = 0 <= cursor;
+ const n = history.length;
+
return (
<>
- <TitleBar label={command ? 'Command Line' : 'Console'}>
- <Label
- className="dimmed"
- display={command && length > 0}
- title="Rank in History"
- >
- {1 + index}/{length}
- </Label>
- <Space />
+ <TitleBar label={edited ? 'Command line' : 'Console'}>
<IconButton
icon="TRASH"
- display={command && clear}
- disabled={!clear}
- onClick={clear}
- title="Clear History"
+ display={edited}
+ disabled={noTrash}
+ onClick={doRemove}
+ title="Discard command from history (irreversible)"
/>
+ <Space />
<IconButton
- icon="CROSS"
- display={command && clear}
- disabled={!current}
- onClick={doDrop}
- title="Remove Command"
+ icon="RELOAD"
+ display={edited}
+ onClick={doReload}
+ title="Discard changes"
/>
- <Space />
<IconButton
icon="MEDIA.PREV"
- display={command}
- disabled={!prev}
+ display={edited}
onClick={doPrev}
- title="Previous Command"
- />
- <IconButton
- icon="RELOAD"
- display={command}
- onClick={doReload}
- title="Reset Command Line"
+ title="Previous command"
/>
<IconButton
icon="MEDIA.NEXT"
- display={command}
- disabled={!next}
+ display={edited}
onClick={doNext}
- title="Next Command"
+ title="Next command"
/>
<Space />
+ <Label
+ className="controller-rank"
+ title="History (last command first)"
+ display={edited}
+ >
+ {1 + cursor} / {n}
+ </Label>
+ <Space />
<IconButton
icon="MEDIA.PLAY"
- display={command}
+ display={edited}
+ disabled={isEmpty}
onClick={doExec}
- title="Execute Command"
+ title="Execute command"
/>
<IconButton
- icon="EDIT"
- selected={command}
- onClick={switchCmd}
- title="Edit Command"
+ icon="TERMINAL"
+ selected={edited}
+ onClick={doSwitch}
+ title="Toggle command line editing"
/>
</TitleBar>
<Text
- buffer={command ? cmdLine : Server.buffer}
+ buffer={edited ? editor : Server.buffer}
mode="text"
- readOnly={!command}
+ readOnly={!edited}
theme="ambiance"
/>
</>
diff --git a/ivette/src/renderer/style.css b/ivette/src/renderer/style.css
index de68fb842c2f4d783486ba20e1ab3b8a65b00792..9b3d079f492d510d53a4b2e990813dd4d2c2103b 100644
--- a/ivette/src/renderer/style.css
+++ b/ivette/src/renderer/style.css
@@ -2,8 +2,9 @@
/* --- Frama-C Styling --- */
/* -------------------------------------------------------------------------- */
-.dimmed {
+.controller-rank {
color: #888 ;
+ min-width: 50px;
}
/* -------------------------------------------------------------------------- */