From 86cf046f7595f9d09d9ae85f577ed677e141ebb6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Nov 2021 15:55:18 +0100
Subject: [PATCH] [ivette] Source code: catches errors on server request.
---
ivette/src/frama-c/kernel/SourceCode.tsx | 14 +++++++++++---
1 file changed, 11 insertions(+), 3 deletions(-)
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 3dbeef14f1a..c9f3d9e0d40 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -105,9 +105,17 @@ export default function SourceCode() {
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 } });
+ try {
+ const [fct, marker] = await Server.send(getMarkerAt, arg);
+ if (fct || marker)
+ updateSelection({ location: { fct, marker } });
+ } catch (err) {
+ D.error(`Failed to get marker from source file position: ${err}`);
+ Status.setMessage({
+ text: 'Failed request to Frama-C server',
+ kind: 'error',
+ });
+ }
}
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
--
GitLab