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

[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.
parent ec916a6a
No related branches found
No related tags found
No related merge requests found
...@@ -65,7 +65,7 @@ function setError(text: string): void { ...@@ -65,7 +65,7 @@ function setError(text: string): void {
} }
// Function launching the external editor at the currently selected position. // 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; if (file === '') return;
const args = cmd const args = cmd
.replace('%s', file) .replace('%s', file)
...@@ -122,7 +122,7 @@ function createEventsHandler(): Editor.Extension { ...@@ -122,7 +122,7 @@ function createEventsHandler(): Editor.Extension {
if (file === '') return; if (file === '') return;
const label = 'Open file in an external editor'; const label = 'Open file in an external editor';
const pos = getCursorPosition(view); 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) => { mouseup: ({ file, command, update }, view, event) => {
if (file === '') return; if (file === '') return;
...@@ -133,7 +133,7 @@ function createEventsHandler(): Editor.Extension { ...@@ -133,7 +133,7 @@ function createEventsHandler(): Editor.Extension {
if (fct || marker) update({ location: { fct, marker } }); if (fct || marker) update({ location: { fct, marker } });
}) })
.catch(() => setError('Failed to request to Frama-C server')); .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 { ...@@ -223,7 +223,7 @@ export default function SourceCode(): JSX.Element {
<Buttons.IconButton <Buttons.IconButton
icon="DUPLICATE" icon="DUPLICATE"
visible={file !== ''} visible={file !== ''}
onClick={() => editor(file, pos, command)} onClick={() => edit(file, pos, command)}
title={externalEditorTitle} title={externalEditorTitle}
/> />
<Labels.Code title={file}>{filename}</Labels.Code> <Labels.Code title={file}>{filename}</Labels.Code>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment