From 115026ba7cd7f2eaa0e9e8ff878220fcb6af0ab2 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Wed, 25 Jan 2023 17:54:33 +0100
Subject: [PATCH] [Ivette] Changing an internal function name
Small detail but the function that starts the external editor is named
"edit", with a verb, like, it's an action.
---
ivette/src/frama-c/kernel/SourceCode.tsx | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 56a8a6a31d7..1e29da3d8fc 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -65,7 +65,7 @@ function setError(text: string): void {
}
// Function launching the external editor at the currently selected position.
-async function editor(file: string, pos: Position, cmd: string): Promise<void> {
+async function edit(file: string, pos: Position, cmd: string): Promise<void> {
if (file === '') return;
const args = cmd
.replace('%s', file)
@@ -122,7 +122,7 @@ function createEventsHandler(): Editor.Extension {
if (file === '') return;
const label = 'Open file in an external editor';
const pos = getCursorPosition(view);
- Dome.popupMenu([ { label, onClick: () => editor(file, pos, command) } ]);
+ Dome.popupMenu([ { label, onClick: () => edit(file, pos, command) } ]);
},
mouseup: ({ file, command, update }, view, event) => {
if (file === '') return;
@@ -133,7 +133,7 @@ function createEventsHandler(): Editor.Extension {
if (fct || marker) update({ location: { fct, marker } });
})
.catch(() => setError('Failed to request to Frama-C server'));
- if (event.ctrlKey) editor(file, pos, command);
+ if (event.ctrlKey) edit(file, pos, command);
},
});
}
@@ -223,7 +223,7 @@ export default function SourceCode(): JSX.Element {
<Buttons.IconButton
icon="DUPLICATE"
visible={file !== ''}
- onClick={() => editor(file, pos, command)}
+ onClick={() => edit(file, pos, command)}
title={externalEditorTitle}
/>
<Labels.Code title={file}>{filename}</Labels.Code>
--
GitLab