From 04a8054562d36639b70d3b044757c3088f8a7bd9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 22 Oct 2021 19:34:06 +0200
Subject: [PATCH] [ivette] Source code: selects the marker at the position of a
left click.
---
ivette/src/frama-c/kernel/SourceCode.tsx | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index d34b86c6047..3dbeef14f1a 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -25,6 +25,7 @@
// --------------------------------------------------------------------------
import React from 'react';
+import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as Dome from 'dome';
@@ -33,7 +34,7 @@ import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { TitleBar } from 'ivette';
import * as Preferences from 'ivette/prefs';
-import { functions, markerInfo } from 'frama-c/api/kernel/ast';
+import { functions, markerInfo, getMarkerAt } from 'frama-c/api/kernel/ast';
import { Code } from 'dome/controls/labels';
import { Hfill } from 'dome/layout/boxes';
import { IconButton } from 'dome/controls/buttons';
@@ -63,7 +64,7 @@ export default function SourceCode() {
// Hooks
const [buffer] = React.useState(new RichTextBuffer());
- const [selection] = States.useSelection();
+ const [selection, updateSelection] = States.useSelection();
const theFunction = selection?.current?.fct;
const theMarker = selection?.current?.marker;
const markersInfo = States.useSyncArray(markerInfo);
@@ -101,6 +102,14 @@ export default function SourceCode() {
type position = CodeMirror.Position;
type editor = CodeMirror.Editor;
+ async function select(_: editor, pos?: position) {
+ if (file === '' || !pos) return;
+ const arg = [file, pos.line + 1, pos.ch + 1];
+ const [fct, marker] = await Server.send(getMarkerAt, arg);
+ if (fct || marker)
+ updateSelection({ location: { fct, marker } });
+ }
+
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
async function launchEditor(_?: editor, pos?: position) {
if (file !== '') {
@@ -162,6 +171,7 @@ export default function SourceCode() {
lineNumbers={!!theFunction}
styleActiveLine={!!theFunction}
extraKeys={{
+ LeftClick: select as (_: CodeMirror.Editor) => void,
'Alt-F': 'findPersistent',
'Ctrl-LeftClick': launchEditor as (_: CodeMirror.Editor) => void,
RightClick: contextMenu as (_: CodeMirror.Editor) => void,
--
GitLab