Skip to content
Snippets Groups Projects
Commit f1c84a29 authored by Maxime Jacquemin's avatar Maxime Jacquemin
Browse files

[Ivette][WIP] Trying to fix synchro bugs on selection

parent a05dfc80
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ivette/src/dome/renderer/text/editor.tsx
+ 43
− 27
View file @ f1c84a29
......@@ -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;
});
}
// -----------------------------------------------------------------------------
......
ivette/src/frama-c/kernel/ASTview.tsx
+ 73
− 21
View file @ f1c84a29
......@@ -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 (
<>
......
ivette/src/frama-c/kernel/SourceCode.tsx
+ 30
− 22
View file @ f1c84a29
......@@ -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>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment