From d41066119d3a24f605ed6cddd2ef45958bdc721a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Oct 2021 10:40:45 +0200
Subject: [PATCH] [ivette] Source code: do not open the external editor when no
file is selected.
---
ivette/src/frama-c/kernel/SourceCode.tsx | 44 +++++++++++++-----------
1 file changed, 24 insertions(+), 20 deletions(-)
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index cea22aa81d0..5ca0ae8143d 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -98,20 +98,22 @@ export default function SourceCode() {
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
async function launchEditor(_: CodeMirror.Editor, pos?: CodeMirror.Position) {
- const selectedLine = pos ? (pos.line + 1).toString() : '1';
- const selectedChar = pos ? (pos.ch + 1).toString() : '1';
- const cmd = command
- .replace('%s', file)
- .replace('%n', selectedLine)
- .replace('%c', selectedChar);
- const args = cmd.split(' ');
- const prog = args.shift();
- if (prog) System.spawn(prog, args).catch(() => {
- Status.setMessage({
- text: `An error has occured when opening the external editor ${prog}`,
- kind: 'error',
+ if (file !== '') {
+ const selectedLine = pos ? (pos.line + 1).toString() : '1';
+ const selectedChar = pos ? (pos.ch + 1).toString() : '1';
+ const cmd = command
+ .replace('%s', file)
+ .replace('%n', selectedLine)
+ .replace('%c', selectedChar);
+ const args = cmd.split(' ');
+ const prog = args.shift();
+ if (prog) System.spawn(prog, args).catch(() => {
+ Status.setMessage({
+ text: `An error has occured when opening the external editor ${prog}`,
+ kind: 'error',
+ });
});
- });
+ }
}
async function contextMenu(
@@ -119,13 +121,15 @@ export default function SourceCode() {
pos?: CodeMirror.Position,
)
{
- const items = [
- {
- label: 'Open file in an external editor',
- onClick: () => launchEditor(editor, pos),
- },
- ];
- Dome.popupMenu(items);
+ if (file !== '') {
+ const items = [
+ {
+ label: 'Open file in an external editor',
+ onClick: () => launchEditor(editor, pos),
+ },
+ ];
+ Dome.popupMenu(items);
+ }
}
// Building the React component.
--
GitLab