diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 64287c759db94780319661e5ab589b55312e9d2a..c2f6cbdab5357bb7eeecb42f8f8ad5b035a8da75 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -24,6 +24,7 @@ import React from 'react';
import { EditorState, StateField, Facet, Extension } from '@codemirror/state';
import { Annotation, Transaction, RangeSet } from '@codemirror/state';
+import { EditorSelection, AnnotationType } from '@codemirror/state';
import { EditorView, ViewPlugin, ViewUpdate } from '@codemirror/view';
import { Decoration, DecorationSet } from '@codemirror/view';
@@ -55,7 +56,8 @@ export type View = EditorView | null;
export type Range = { from: number, to: number };
export type Set<A> = (view: View, value: A) => void;
export type Get<A> = (state: EditorState | undefined) => A;
-export interface Data<A, S> { init: A, get: Get<A>, structure: S }
+export interface Structure<S> { structure: S, extension: Extension }
+export interface Data<A, S> extends Structure<S> { init: A, get: Get<A> }
// Event handlers type definition.
export type Handler<I, E> = (i: I, v: EditorView, e: E) => void;
@@ -70,7 +72,7 @@ export type Handlers<I> = { [e in keyof EventMap]?: Handler<I, EventMap[e]> };
// structure is exposed for two reasons. The first one is that it contains the
// extension that must be added to the CodeMirror instanciation. The second one
// is that it is needed during the Aspects creation's process.
-export interface Field<A> extends Data<A, StateField<A>> { set: Set<A> }
+export interface Field<A> extends Data<A, StateField<A>> { set: Set<A>, annotation: AnnotationType<A> }
// An Aspect is a data associated with an editor state and computed by combining
// data from several fields. A typical use case is if one needs a data that
@@ -79,7 +81,7 @@ export interface Field<A> extends Data<A, StateField<A>> { set: Set<A> }
// information of CodeMirror) is changed. An Aspect exposes a getter that
// handles all React's hooks shenanigans and an extension that must be added to
// the CodeMirror initial configuration.
-export interface Aspect<A> extends Data<A, Facet<A, A>> { extension: Extension }
+export interface Aspect<A> extends Data<A, Facet<A, A>> {}
// State extensions and Aspects have to declare their dependencies, i.e. the
// Field and Aspects they rely on to perform their computations. Dependencies
@@ -128,15 +130,6 @@ function inputs<I extends Dict>(ds: Deps<I>, s: EditorState | undefined): Dict {
return transformDict(ds, (d) => d.get(s));
}
-// Helper function retrieving a dependency extension.
-function getExtension<A>(dep: Dependency<A>): Extension {
- type Dep<A> = Dependency<A>;
- const asExt = (d: Dep<A>): boolean => Object.keys(d).includes('extension');
- const isAspect = (d: Dep<A>): d is Aspect<A> => asExt(d);
- if (isAspect(dep)) return dep.extension;
- else return dep.structure.extension;
-}
-
// -----------------------------------------------------------------------------
@@ -170,9 +163,8 @@ export function createField<A>(init: A): Field<A> {
const update: Update<A> = (current, tr) => tr.annotation(annot) ?? current;
const field = StateField.define<A>({ create, update });
const get: Get<A> = (state) => state?.field(field) ?? init;
- const useSet: Set<A> = (v, a) =>
- React.useEffect(() => v?.dispatch({ annotations: annot.of(a) }), [v, a]);
- return { init, get, set: useSet, structure: field };
+ const set: Set<A> = (v, a) => v?.dispatch({ annotations: annot.of(a) });
+ return { init, get, set, structure: field, extension: field, annotation: annot };
}
// An Aspect is declared using its dependencies and a function. This function's
@@ -183,7 +175,7 @@ export function createAspect<I extends Dict, O>(
deps: Dependencies<I>,
fn: (input: I) => O,
): Aspect<O> {
- const enables = mapDict(deps, getExtension);
+ const enables = mapDict(deps, (d) => d.extension);
const init = fn(transformDict(deps, (d) => d.init) as I);
const combine: Combine<O> = (l) => l.length > 0 ? l[l.length - 1] : init;
const facet = Facet.define<O, O>({ combine, enables });
@@ -201,7 +193,7 @@ export function createDecorator<I extends Dict>(
deps: Dependencies<I>,
fn: (inputs: I, state: EditorState) => DecorationSet
): Extension {
- const enables = mapDict(deps, getExtension);
+ const enables = mapDict(deps, (d) => d.extension);
const get = (s: EditorState): DecorationSet => fn(inputs(deps, s) as I, s);
class S { s: DecorationSet = RangeSet.empty; }
class D extends S { update(u: ViewUpdate): void { this.s = get(u.state); } }
@@ -217,7 +209,7 @@ export function createGutter<I extends Dict>(
className: string,
line: (inputs: I, block: Range, view: EditorView) => GutterMarker | null
): Extension {
- const enables = mapDict(deps, getExtension);
+ const enables = mapDict(deps, (d) => d.extension);
const extension = gutter({
class: className,
lineMarker: (view, block) => {
@@ -250,7 +242,7 @@ export function createEventHandler<I extends Dict>(
deps: Dependencies<I>,
handlers: Handlers<I>,
): Extension {
- const enables = mapDict(deps, getExtension);
+ const enables = mapDict(deps, (d) => d.extension);
const domEventHandlers = Object.fromEntries(Object.keys(handlers).map((k) => {
const h = handlers[k] as Handler<I, typeof k>;
const fn = (e: typeof k, v: EditorView): void =>
@@ -260,6 +252,10 @@ export function createEventHandler<I extends Dict>(
return enables.concat(EditorView.domEventHandlers(domEventHandlers));
}
+export function createUpdater(fn: (update: ViewUpdate) => void): Extension {
+ return EditorView.updateListener.of(fn);
+}
+
// -----------------------------------------------------------------------------
@@ -304,20 +300,32 @@ export const LanguageHighlighter: Extension =
// Standard extensions and commands
// -----------------------------------------------------------------------------
+export const Selection = createSelectionField();
+function createSelectionField(): Field<EditorSelection> {
+ const cursor = EditorSelection.cursor(0);
+ const field = createField<EditorSelection>(EditorSelection.create([cursor]));
+ const set: Set<EditorSelection> = (view, selection) => {
+ field.set(view, selection);
+ view?.dispatch({ selection });
+ }
+ const updater = EditorView.updateListener.of((update) => {
+ if (update.selectionSet) field.set(update.view, update.state.selection);
+ });
+ return { ...field, set, extension: [field.extension, updater] };
+}
+
// Create a text field that updates the CodeMirror document when set.
export type ToString<A> = (text: A) => string;
export function createTextField<A>(init: A, toString: ToString<A>): Field<A> {
const field = createField<A>(init);
- const useSet: Set<A> = (view, text) => {
+ const set: Set<A> = (view, text) => {
field.set(view, text);
- React.useEffect(() => {
- const selection = { anchor: 0 };
- const length = view?.state.doc.length;
- const changes = { from: 0, to: length, insert: toString(text) };
- view?.dispatch({ changes, selection });
- }, [view, text]);
+ const selection = { anchor: 0 };
+ const length = view?.state.doc.length;
+ const changes = { from: 0, to: length, insert: toString(text) };
+ view?.dispatch({ changes, selection });
};
- return { ...field, set: useSet };
+ return { ...field, set };
}
// An extension displaying line numbers in a gutter. Does not display anything
@@ -375,6 +383,14 @@ export function selectLine(view: View, line: number, atTop: boolean): void {
view.dispatch({ effects });
}
+export const TransactionExtenderTest = createTest();
+function createTest(): Extension {
+ return EditorState.transactionExtender.of((transaction) => {
+ console.log(transaction);
+ return null;
+ });
+}
+
// -----------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index f52c60997293e9ab52c3ecae6757ed502ac7e620..ac8f6105960d1bfedd37e5d2a28afff3d3604b3d 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -62,7 +62,7 @@ type Range = Editor.Range;
function isDef<A>(a: A | undefined): a is A { return a !== undefined; }
// Map a function over a list, removing all inputs that returned undefined.
-function mapFilter<A, B>(xs: A[], fn: (x: A) => B | undefined): B[] {
+function mapFilter<A, B>(xs: readonly A[], fn: (x: A) => B | undefined): B[] {
return xs.map(fn).filter(isDef);
}
@@ -149,6 +149,27 @@ function coveringNode(tree: Tree, pos: number): Node | undefined {
// -----------------------------------------------------------------------------
+/*
+function useViewState() {
+ const [selection, updateSelection] = States.useSelection();
+ const [hovered, updateHovered] = States.useHovered();
+ const selected = selection?.current?.marker;
+ const fct = selection?.current?.fct;
+
+ const text = States.useRequest(Ast.printFunction, fct) ?? null;
+ const tree = React.useMemo(() => textToTree(text) ?? empty, [text]);
+ const ranges = React.useMemo(() => markersRanges(tree), [tree]);
+ const code = React.useMemo(() => textToString(text), [text]);
+
+ const emptyDead = { unreachable: [], nonTerminating: [] };
+ const dead = States.useRequest(Eva.getDeadCode, fct) ?? emptyDead;
+ const tags = States.useTags(Properties.propStatusTags);
+ const propertiesStatuses = States.useSyncArray(Properties.status).getArray();
+
+
+}
+*/
+
// -----------------------------------------------------------------------------
// Function code representation
@@ -204,18 +225,38 @@ function createMarkerUpdater(): Editor.Extension {
});
}
+const MarkerScroller = Editor.createUpdater((update) => {
+ console.log(update);
+ const a = Marker.annotation;
+ const markers = mapFilter(update.transactions, (tr) => tr.annotation(a));
+ if (markers.length !== 1) return;
+ const marker = markers[0];
+ const selection = update.state.selection.main;
+ const ranges = Ranges.get(update.state).get(marker) ?? [];
+ if (ranges.length !== 1) { console.log(ranges); return; }
+ if (ranges[0] === selection) return;
+ const { from: anchor } = ranges[0];
+ update.view.dispatch({ selection: { anchor }, scrollIntoView: true });
+});
+
+
+/*
// Scroll the selected marker into view if needed. Used for when the marker is
// changed outside of this component.
function scrollMarkerIntoView(view: Editor.View, marker: Marker): void {
if (!view || !marker) return;
const selection = view.state.selection.main;
+ console.log('-- Marker: ', marker);
const ranges = Ranges.get(view.state).get(marker) ?? [];
+ console.log('-- Ranges: ', ranges);
if (ranges.length === 0) return;
const exists = ranges.find((range) => range === selection);
+ console.log('-- Exists: ', exists);
if (exists) return;
const { from: anchor } = ranges[0];
view.dispatch({ selection: { anchor }, scrollIntoView: true });
}
+*/
// -----------------------------------------------------------------------------
@@ -597,7 +638,10 @@ function useFctDead(fct: Fct): Eva.deadCode {
// Server request handler returning the given function's callers.
function useFctCallers(fct: Fct): Caller[] {
const callers = States.useRequest(Eva.getCallers, fct) ?? [];
- return callers.map(([fct, marker]) => ({ fct, marker }));
+ const res = React.useMemo(() => {
+ return callers.map(([fct, marker]) => ({ fct, marker }))
+ }, [callers]);
+ return res;
}
// Server request handler returning the tainted lvalues.
@@ -616,6 +660,7 @@ function useFctTaints(fct: Fct): Eva.LvalueTaints[] {
// Necessary extensions for our needs.
const extensions: Editor.Extension[] = [
MarkerUpdater,
+ // MarkerScroller,
HoveredUpdater,
CodeDecorator,
DeadCodeDecorator,
@@ -625,6 +670,7 @@ const extensions: Editor.Extension[] = [
TaintTooltip,
Editor.FoldGutter,
Editor.LanguageHighlighter,
+ Editor.TransactionExtenderTest,
];
// The component in itself.
@@ -633,38 +679,44 @@ export default function ASTview(): JSX.Element {
const { view, Component } = Editor.Editor(extensions);
// Updating CodeMirror when the selection or its callback are changed.
- const [selection, updateSelection] = States.useSelection();
- UpdateSelection.set(view, updateSelection);
+ const [selection, setSel] = States.useSelection();
+ React.useEffect(() => UpdateSelection.set(view, setSel), [view, setSel]);
+ const fct = selection?.current?.fct;
+ React.useEffect(() => Fct.set(view, fct), [view, fct]);
+ const marker = selection?.current?.marker;
+ React.useEffect(() => Marker.set(view, marker), [view, marker]);
// Updating CodeMirror when the <updateHovered> callback is changed.
- const [hovered, updateHovered] = States.useHovered();
- UpdateHovered.set(view, updateHovered);
+ const [hov, setHov] = States.useHovered();
+ React.useEffect(() => UpdateHovered.set(view, setHov), [view, setHov]);
+ React.useEffect(() => Hovered.set(view, hov?.marker ?? ''), [view, hov]);
// Updating CodeMirror when the <properties> synchronized array is changed.
- const properties = States.useSyncArray(Properties.status).getArray();
- PropertiesStatuses.set(view, properties);
+ const props = States.useSyncArray(Properties.status).getArray();
+ React.useEffect(() => PropertiesStatuses.set(view, props), [view, props]);
// Updating CodeMirror when the <propStatusTags> map is changed.
const tags = States.useTags(Properties.propStatusTags);
- Tags.set(view, tags);
+ React.useEffect(() => Tags.set(view, tags), [view, tags]);
// Updating CodeMirror when the <markersInfo> synchronized array is changed.
const info = States.useSyncArray(Ast.markerInfo);
- const getMarkerData = React.useCallback((key) => info.getData(key), [info]);
- GetMarkerData.set(view, getMarkerData);
+ const getData = React.useCallback((key) => info.getData(key), [info]);
+ React.useEffect(() => GetMarkerData.set(view, getData), [view, getData]);
// Retrieving data on currently selected function and updating CodeMirror when
// they have changed.
- const fct = selection?.current?.fct;
- const marker = selection?.current?.marker;
- Text.set(view, useFctText(fct));
- Fct.set(view, fct);
- Marker.set(view, marker);
- Hovered.set(view, hovered?.marker ?? '');
- Dead.set(view, useFctDead(fct));
- Callers.set(view, useFctCallers(fct));
- TaintedLvalues.set(view, useFctTaints(fct));
- React.useEffect(() => scrollMarkerIntoView(view, marker), [view, marker]);
+ const text = useFctText(fct);
+ React.useEffect(() => Text.set(view, text), [view, text]);
+ // const dead = useFctDead(fct);
+ // React.useEffect(() => Dead.set(view, dead), [view, dead]);
+ // const callers = useFctCallers(fct);
+ // React.useEffect(() => Callers.set(view, callers), [view, callers]);
+ // const taints = useFctTaints(fct);
+ // React.useEffect(() => TaintedLvalues.set(view, taints), [view, taints]);
+
+ // Scrolling the selected marker into view if needed.
+ // React.useEffect(() => scrollMarkerIntoView(view, marker), [view, marker]);
return (
<>
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 05cb75e067bbb82a96ec061a335b42c1df456c3a..56a8a6a31d777b0b07ec549b1fd226b0abad0de5 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -45,6 +45,10 @@ import * as Preferences from 'ivette/prefs';
// Utilitary types and functions
// -----------------------------------------------------------------------------
+// An alias type for functions and locations.
+type Fct = string | undefined;
+type Marker = string | undefined;
+
// Recovering the cursor position as a line and a column.
interface Position { line: number, column: number }
function getCursorPosition(view: Editor.View): Position {
@@ -61,15 +65,12 @@ function setError(text: string): void {
}
// Function launching the external editor at the currently selected position.
-interface LaunchEditorProps { view: Editor.View, file: string, command: string }
-async function launchEditor(props: LaunchEditorProps): Promise<void> {
- const { view, file, command } = props;
- if (!view || file === '') return;
- const { line: l, column: c } = getCursorPosition(view);
- const args = command
+async function editor(file: string, pos: Position, cmd: string): Promise<void> {
+ if (file === '') return;
+ const args = cmd
.replace('%s', file)
- .replace('%n', l.toString())
- .replace('%c', c.toString())
+ .replace('%n', pos.line.toString())
+ .replace('%c', pos.column.toString())
.split(' ');
const prog = args.shift(); if (!prog) return;
const text = `An error has occured when opening the external editor ${prog}`;
@@ -93,11 +94,15 @@ const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
const Source = Editor.createTextField<string>('', (s) => s);
const File = Editor.createField<string>('');
-// const Line = Editor.createLineField();
-
// This field contains the command use to start the external editor.
const Command = Editor.createField<string>('');
+// This field contains the currently selected function.
+const Fct = Editor.createField<Fct>(undefined);
+
+// This field contains the currently selected marker.
+const Marker = Editor.createField<Marker>(undefined);
+
// -----------------------------------------------------------------------------
@@ -115,20 +120,20 @@ function createEventsHandler(): Editor.Extension {
return Editor.createEventHandler(deps, {
contextmenu: ({ file, command }, view) => {
if (file === '') return;
- const launch = (): Promise<void> => launchEditor({ view, file, command });
const label = 'Open file in an external editor';
- Dome.popupMenu([ { label, onClick: launch } ]);
+ const pos = getCursorPosition(view);
+ Dome.popupMenu([ { label, onClick: () => editor(file, pos, command) } ]);
},
mouseup: ({ file, command, update }, view, event) => {
if (file === '') return;
- const { line, column } = getCursorPosition(view);
+ const pos = getCursorPosition(view);
Server
- .send(Ast.getMarkerAt, [file, line, column])
+ .send(Ast.getMarkerAt, [file, pos.line, pos.column])
.then(([fct, marker]) => {
if (fct || marker) update({ location: { fct, marker } });
})
.catch(() => setError('Failed to request to Frama-C server'));
- if (event.ctrlKey) launchEditor({ view, file, command });
+ if (event.ctrlKey) editor(file, pos, command);
},
});
}
@@ -158,7 +163,8 @@ function useFctSource(file: string): string {
// Necessary extensions.
const extensions: Editor.Extension[] = [
- Source.structure,
+ Source,
+ Editor.Selection,
Editor.LineNumbers,
Editor.LanguageHighlighter,
Editor.HighlightActiveLine,
@@ -182,7 +188,7 @@ export default function SourceCode(): JSX.Element {
const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
const { view, Component } = Editor.Editor(extensions);
- const [selection, updateSelection] = States.useSelection();
+ const [selection, update] = States.useSelection();
const marker = selection?.current?.marker;
const fct = selection?.current?.fct;
const displayedFct = React.useRef<string | undefined>(undefined);
@@ -191,11 +197,13 @@ export default function SourceCode(): JSX.Element {
const fctSloc = useFunctionLocation(fct);
const file = fctSloc?.file ?? '';
const filename = Path.parse(file).base;
+ const pos = getCursorPosition(view);
+ const source = useFctSource(file);
- Source.set(view, useFctSource(file));
- UpdateSelection.set(view, updateSelection);
- Command.set(view, command);
- File.set(view, file);
+ React.useEffect(() => Source.set(view, source), [view, source]);
+ React.useEffect(() => UpdateSelection.set(view, update), [view, update]);
+ React.useEffect(() => Command.set(view, command), [view, command]);
+ React.useEffect(() => File.set(view, file), [view, file]);
React.useEffect(() => {
const notDisplayedFct = fct !== displayedFct.current;
@@ -215,7 +223,7 @@ export default function SourceCode(): JSX.Element {
<Buttons.IconButton
icon="DUPLICATE"
visible={file !== ''}
- onClick={() => launchEditor({ view, file, command })}
+ onClick={() => editor(file, pos, command)}
title={externalEditorTitle}
/>
<Labels.Code title={file}>{filename}</Labels.Code>