diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 587aded505b38fed77c44cd045c22b139fd20e78..188789ffcbaf7df48cb2817750f90db55194aef0 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -375,6 +375,26 @@ function createSelectionField(): Field<EditorSelection> {
return { ...field, set, extension: [field.extension, updater] };
}
+export type RangeCallback = (offset: number, endOffset: number) => void;
+export const OnSelection = createOnSelectionField();
+function createOnSelectionField(): Field<RangeCallback|null> {
+ const field = createField<RangeCallback|null>(null);
+ const set: Set<RangeCallback|null> = (view, fn) => {
+ field.set(view, fn);
+ };
+ const updater = EditorView.updateListener.of((update) => {
+ if (update.selectionSet) {
+ const view = update.view;
+ const fn = field.get(view.state);
+ if (fn !== null) {
+ const { from: offset, to: endOffset } = view.state.selection.main;
+ fn(offset, endOffset);
+ }
+ }
+ });
+ return { ...field, set, extension: [field.extension, updater] };
+}
+
export const Document = createDocumentField();
function createDocumentField(): Field<Text> {
const field = createField<Text>(Text.empty);
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 4b1de459df7ef913508013b05d0574faa450b6a7..ab59483b78641a4cccc8a2884be9aa046deffc3e 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -21,7 +21,6 @@
/* ************************************************************************ */
import React from 'react';
-import * as Path from 'path';
import * as Dome from 'dome';
import * as System from 'dome/system';
@@ -32,39 +31,34 @@ import * as Buttons from 'dome/controls/buttons';
import * as Dialogs from 'dome/dialogs';
import * as Toolbars from 'dome/frame/toolbars';
-import { Selection, Document } from 'dome/text/editor';
+import * as Ivette from 'ivette';
+import * as Preferences from 'ivette/prefs';
-import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as Status from 'frama-c/kernel/Status';
import * as Ast from 'frama-c/kernel/api/ast';
-import * as Ivette from 'ivette';
-import * as Preferences from 'ivette/prefs';
-
-
-
// -----------------------------------------------------------------------------
// Utilitary types and functions
// -----------------------------------------------------------------------------
-// Recovering the cursor position as a line and a column.
interface Position { line: number, column: number }
+
+// Recovering the cursor position as a line and a column.
function getCursorPosition(view: Editor.View): Position {
const pos = view?.state.selection.main;
if (!view || !pos) return { line: 1, column: 1 };
const line = view.state.doc.lineAt(pos.from);
- const column = pos.from - line.from + 1;
+ const column = pos.from - line.from;
return { line: line.number, column };
}
-// Error messages.
-function setError(text: string): void {
- Status.setMessage({ text, kind: 'error' });
-}
-
// Function launching the external editor at the currently selected position.
-async function edit(file: string, pos: Position, cmd: string): Promise<void> {
+async function editSourceFile(
+ cmd: string,
+ file: string,
+ pos: Position
+): Promise<void> {
if (file === '') return;
const args = cmd
.replace('%s', file)
@@ -72,156 +66,90 @@ async function edit(file: string, pos: Position, cmd: string): Promise<void> {
.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}`;
- System.spawn(prog, args).catch(() => setError(text));
+ System.spawn(prog, args).catch(() => {
+ const text = 'Editing Failed';
+ const title = `Command ${prog} ${args} failed.`;
+ Status.setMessage({ text, title, kind: 'error' });
+ });
}
-// -----------------------------------------------------------------------------
-
+// Editor Help popup
+async function displayShortcuts(): Promise<void> {
+ await Dialogs.showMessageBox({
+ buttons: [{ label: "Ok" }],
+ details: (
+ 'Ctrl+click: open file in an external editor at the selected location.\n'
+ + 'Alt+f: search for text or regexp.\n'
+ + 'Alt+g: go to line.'
+ ),
+ message: 'Useful shortcuts',
+ });
+}
+// Toplevel Declaration Markers
+function isToplevelDecl(kind: Ast.markerKind): boolean {
+ switch(kind) {
+ case 'DFUN':
+ case 'DECLARATION':
+ return true;
+ default:
+ return false;
+ }
+}
// -----------------------------------------------------------------------------
-// Fields declarations
+// Selection Events
// -----------------------------------------------------------------------------
-// Those fields contain the source code and the file name.
-const Source = Editor.createTextField<string>('', (s) => s);
-const File = Editor.createField<string>('');
+type SourceCursor = { file: string, line: number, column: number };
+type SourceCallback = ((pos: Position) => void) | null;
-// This field contains the command use to start the external editor.
-const Command = Editor.createField<string>('');
+const noCursor: SourceCursor = { file: '', line: 0, column: 0 };
+const OnSelection = Editor.OnSelection;
+const OnControlClick = Editor.createField<SourceCallback>(null);
+const OnContextMenu = Editor.createField<SourceCallback>(null);
-// These field contains a callback that returns the source of a location.
-type GetSource = (loc: States.Location) => Ast.source | undefined;
-const GetSource = Editor.createField<GetSource>(() => undefined);
-
-// We keep track of the cursor location (i.e the location that is under the
-// current CodeMirror cursor) and the ivette location (i.e the locations as
-// seen by the outside world). Keeping track of both of them together force
-// their update in one dispatch, which prevents strange bugs.
-interface Locations { cursor?: States.Location, current: States.Location }
-
-// The Locations field. When given Locations, it will update the cursor field if
-// and only if the new cursor location is not undefined. It simplifies the
-// update in the SourceCode component itself.
-const Locations = createLocationsField();
-function createLocationsField(): Editor.Field<Locations> {
- const noField = { cursor: undefined, current: {} };
- const field = Editor.createField<Locations>(noField);
- const set: Editor.Set<Locations> = (view, toBe) => {
- const hasBeen = field.get(view?.state);
- const cursor = toBe.cursor ?? hasBeen.cursor;
- field.set(view, { cursor, current: toBe.current });
+// This events handler takes care of mouse events
+const EventHandlers = createEventHandlers();
+function createEventHandlers(): Editor.Extension {
+ const deps = {
+ onControlClick: OnControlClick,
+ onContextMenu: OnContextMenu
};
- return { ...field, set };
-}
-
-// -----------------------------------------------------------------------------
-
-
-
-// -----------------------------------------------------------------------------
-// Synchronisation with the outside world
-// -----------------------------------------------------------------------------
-
-// Update the outside world when the user click somewhere in the source code.
-const SyncOnUserSelection = createSyncOnUserSelection();
-function createSyncOnUserSelection(): Editor.Extension {
- const actions = { cmd: Command };
- const deps = { file: File, selection: Selection, doc: Document, ...actions };
return Editor.createEventHandler(deps, {
- mouseup: async ({ file, cmd }, view, event) => {
- if (!view || file === '') return;
- const pos = getCursorPosition(view);
- const cursor = { file, line: pos.line, column: pos.column };
- try {
- const marker = await Server.send(Ast.getMarkerAt, cursor);
- if (marker) {
- // The forced reload should NOT be necessary but... It is...
- await Server.send(Ast.reloadMarkerAttributes, null);
- States.setSelected(marker);
- const scope = States.getMarker(marker)?.scope;
- const location = { marker, scope };
- Locations.set(view, { cursor: location, current: location });
- }
- } catch {
- setError('Failure');
+ // Control Click
+ mouseup: ({ onControlClick }, view, event) => {
+ if (event.ctrlKey && onControlClick !== null) {
+ const pos = getCursorPosition(view);
+ onControlClick(pos);
+ }
+ },
+ // Context Menu
+ contextmenu: ({ onContextMenu }, view) => {
+ if (onContextMenu !== null) {
+ const pos = getCursorPosition(view);
+ onContextMenu(pos);
}
- if (event.ctrlKey) edit(file, pos, cmd);
}
});
}
-// Update the cursor position when the outside world changes the selected
-// location.
-const SyncOnOutsideSelection = createSyncOnOutsideSelection();
-function createSyncOnOutsideSelection(): Editor.Extension {
- const deps = { locations: Locations, get: GetSource };
- return Editor.createViewUpdater(deps, ({ locations, get }, view) => {
- const { cursor, current } = locations;
- if (current === undefined || current === cursor) return;
- const source = get(current); if (!source) return;
- const newDecl =
- current.scope !== cursor?.scope && current.marker === undefined;
- const onTop = cursor === undefined || newDecl;
- Locations.set(view, { cursor: current, current });
- Editor.selectLine(view, source.line, onTop, false);
- });
-}
-
// -----------------------------------------------------------------------------
-
-
-
-// -----------------------------------------------------------------------------
-// Context menu
-// -----------------------------------------------------------------------------
-
-// This events handler takes care of the context menu.
-const ContextMenu = createContextMenu();
-function createContextMenu(): Editor.Extension {
- const deps = { file: File, command: Command };
- return Editor.createEventHandler(deps, {
- contextmenu: ({ file, command }, view) => {
- if (file === '') return;
- const label = 'Open file in an external editor';
- const pos = getCursorPosition(view);
- Dome.popupMenu([ { label, onClick: () => edit(file, pos, command) } ]);
- },
- });
-}
-
+// Source File Contents
// -----------------------------------------------------------------------------
+const Source = Editor.createTextField<string>('', (s: string) => s);
-
-// -----------------------------------------------------------------------------
-// Server requests
-// -----------------------------------------------------------------------------
-
-// Server request handler returning the source code.
-function useFctSource(file: string): string {
- const req = React.useMemo(() => System.readFile(file), [file]);
+// System request to read the source file.
+function useSourceFileContents(file: string | undefined): string {
+ const req = React.useMemo(() => {
+ if (!file) return Promise.resolve('');
+ return System.readFile(file);
+ }, [file]);
const { result } = Dome.usePromise(req);
return result ?? '';
}
-// Build a callback that retrieves a location's source information.
-function useSourceGetter(): GetSource {
- const getAttr = States.useSyncArrayGetter(Ast.markerAttributes);
- const getDecl = States.useSyncArrayGetter(Ast.declAttributes);
- return React.useCallback(({ scope, marker }) => {
- const { sloc, scope: markerDecl } = getAttr(marker) ?? {};
- if (sloc) return sloc;
- const { source } = getDecl(scope ?? markerDecl) ?? {};
- return source;
- }, [getAttr, getDecl]);
-}
-
-// -----------------------------------------------------------------------------
-
-
-
// -----------------------------------------------------------------------------
// Source Code component
// -----------------------------------------------------------------------------
@@ -235,10 +163,10 @@ const extensions: Editor.Extension[] = [
Editor.LineNumbers,
Editor.LanguageHighlighter,
Editor.HighlightActiveLine,
- SyncOnUserSelection,
- SyncOnOutsideSelection,
- ContextMenu,
- Locations.structure,
+ OnSelection,
+ OnContextMenu,
+ OnControlClick,
+ EventHandlers,
];
// The component in itself.
@@ -246,52 +174,71 @@ 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 current = States.useCurrentLocation();
- const getSource = useSourceGetter();
- const file = getSource(current)?.file ?? '';
- const filename = Path.parse(file).base;
- const pos = getCursorPosition(view);
- const source = useFctSource(file);
+ const selectedMarker = States.useSelected();
+ const { sloc, kind } = States.useMarker(selectedMarker);
+ const [floc, setFloc] = React.useState<Ast.source | undefined>();
+ const isTop = isToplevelDecl(kind);
+ React.useEffect(() => { if (sloc) setFloc(sloc); }, [sloc]);
+ const file = floc?.file;
+ const filename = floc?.base;
+ const selectedMarkerLine = floc?.line ?? 0;
+ const source = useSourceFileContents(file);
+ const [cursor, setCursor] = React.useState<SourceCursor>(noCursor);
+ const markerAtCursor = States.useRequest(Ast.getMarkerAt, cursor);
+ const { sloc: slocAtCursor } = States.useMarker(markerAtCursor);
+
+ const editFile = React.useCallback(() => {
+ if (file) editSourceFile(command, file, getCursorPosition(view));
+ }, [ command, file, view ]
+ );
- React.useEffect(() => GetSource.set(view, getSource), [view, getSource]);
- React.useEffect(() => File.set(view, file), [view, file]);
+ const menuPopup = React.useCallback(() => {
+ if (file && command)
+ Dome.popupMenu([{
+ label: 'Edit file in editor',
+ onClick: editFile,
+ }]);
+ }, [file, command, editFile] );
+
+ const onSelect = React.useCallback((offset, endOffset) => {
+ if (!view || !file || endOffset !== offset) return;
+ const theLine = view.state.doc.lineAt(offset);
+ const line = theLine.number;
+ const column = offset - theLine.from;
+ setCursor({ file, line, column });
+ }, [view, file]);
+
+ React.useEffect(() => { if (!file) setCursor(noCursor); }, [file]);
React.useEffect(() => Source.set(view, source), [view, source]);
- React.useEffect(() => Command.set(view, command), [view, command]);
- React.useEffect(() => Locations.set(view, { current }), [view, current]);
+ React.useEffect(() => OnSelection.set(view, onSelect), [view, onSelect]);
+ React.useEffect(() => OnContextMenu.set(view, menuPopup), [view, menuPopup]);
+ React.useEffect(() => OnControlClick.set(view, editFile), [view, editFile]);
- const externalEditorTitle =
- 'Open the source file in an external editor.';
+ React.useEffect(() => {
+ if (selectedMarkerLine > 0)
+ Editor.selectLine(view, selectedMarkerLine, isTop, true);
+ }, [view, isTop, selectedMarkerLine]);
- const shortcuts =
- 'Ctrl+click: open file in an external editor at the selected location.\n'
- + 'Alt+f: search for text or regexp.\n'
- + 'Alt+g: go to line.';
-
- const shortcutsTitle = 'Useful shortcuts:\n' + shortcuts;
-
- async function displayShortcuts(): Promise<void> {
- await Dialogs.showMessageBox({
- buttons: [{ label: "Ok" }],
- details: shortcuts,
- message: 'Useful shortcuts'
- });
- }
+ React.useEffect(() => {
+ if (cursor.line === slocAtCursor?.line)
+ States.setSelected(markerAtCursor);
+ }, [cursor, markerAtCursor, slocAtCursor]);
return (
<>
<Ivette.TitleBar>
<Buttons.IconButton
icon="DUPLICATE"
- visible={file !== ''}
- onClick={() => edit(file, pos, command)}
- title={externalEditorTitle}
+ visible={!file}
+ onClick={editFile}
+ title='externalEditorTitle'
/>
<Labels.Code title={file}>{filename}</Labels.Code>
<Toolbars.Filler />
<Buttons.IconButton
icon="HELP"
onClick={displayShortcuts}
- title={shortcutsTitle}
+ title='Useful shortcuts'
/>
<Toolbars.Inset/>
</Ivette.TitleBar>
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index a279ce2d235862096fdea3a5fad367c46fceb442..749c722b9e3696443416bc200738568f601d9ff8 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -558,7 +558,7 @@ const getMarkerAt_internal: Server.GetRequest<
output: Json.jOption(jMarker),
signals: [ { name: 'kernel.ast.changed' } ],
};
-/** Returns the marker and function at a source file position, if any. Input: file path, line and column. */
+/** Returns the marker and function at a source file position, if any. Input: file path, line and column. File can be empty, in case no marker is returned. */
export const getMarkerAt: Server.GetRequest<
{ file: string, line: number, column: number },
marker |
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 109d8849e03a5f5fa4ab6b48ff796c39eb73f173..34f517c581b91ba276b112605784e14dca9fe94c 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -899,26 +899,28 @@ let () = Server_parameters.Debug.add_hook_on_update
(* -------------------------------------------------------------------------- *)
let get_marker_at ~file ~line ~col =
- let pos_path = Filepath.Normalized.of_string file in
- let pos =
- Filepath.{ pos_path; pos_lnum = line; pos_cnum = col; pos_bol = 0; }
- in
- Printer_tag.loc_to_localizable ~precise_col:true pos
+ if file="" then None else
+ let pos_path = Filepath.Normalized.of_string file in
+ let pos =
+ Filepath.{ pos_path; pos_lnum = line; pos_cnum = col; pos_bol = 0; }
+ in
+ Printer_tag.loc_to_localizable ~precise_col:true pos
let () =
let descr =
Md.plain
"Returns the marker and function at a source file position, if any. \
- Input: file path, line and column."
+ Input: file path, line and column. \
+ File can be empty, in case no marker is returned."
in
let signature = Request.signature
~output:(module Joption(Marker)) () in
let get_file = Request.param signature
~name:"file" ~descr:(Md.plain "File path") (module Jstring) in
let get_line = Request.param signature
- ~name:"line" ~descr:(Md.plain "Line number") (module Jint) in
+ ~name:"line" ~descr:(Md.plain "Line (1-based)") (module Jint) in
let get_col = Request.param signature
- ~name:"column" ~descr:(Md.plain "Column number") (module Jint) in
+ ~name:"column" ~descr:(Md.plain "Column (0-based)") (module Jint) in
Request.register_sig signature
~package ~descr ~kind:`GET ~name:"getMarkerAt"
~signals:[ast_changed_signal]