From 4c9adb69f01a2e8ba38b65d70970f8dc15f48ce2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 Oct 2021 12:56:10 +0200
Subject: [PATCH] [ivette] Source code: adds a toolbar button to open the file
in an editor.
---
ivette/src/frama-c/kernel/SourceCode.tsx | 26 +++++++++++++++++-------
1 file changed, 19 insertions(+), 7 deletions(-)
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 5ca0ae8143d..d34b86c6047 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -36,6 +36,7 @@ import * as Preferences from 'ivette/prefs';
import { functions, markerInfo } from 'frama-c/api/kernel/ast';
import { Code } from 'dome/controls/labels';
import { Hfill } from 'dome/layout/boxes';
+import { IconButton } from 'dome/controls/buttons';
import * as Path from 'path';
import * as Settings from 'dome/data/settings';
import * as Status from 'frama-c/kernel/Status';
@@ -96,8 +97,12 @@ export default function SourceCode() {
React.useEffect(() => buffer.setValue(result), [buffer, result]);
React.useEffect(() => buffer.setCursorOnTop(line), [buffer, line, result]);
+ /* CodeMirror types used to bind callbacks to extraKeys. */
+ type position = CodeMirror.Position;
+ type editor = CodeMirror.Editor;
+
const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
- async function launchEditor(_: CodeMirror.Editor, pos?: CodeMirror.Position) {
+ async function launchEditor(_?: editor, pos?: position) {
if (file !== '') {
const selectedLine = pos ? (pos.line + 1).toString() : '1';
const selectedChar = pos ? (pos.ch + 1).toString() : '1';
@@ -116,11 +121,7 @@ export default function SourceCode() {
}
}
- async function contextMenu(
- editor: CodeMirror.Editor,
- pos?: CodeMirror.Position,
- )
- {
+ async function contextMenu(editor?: editor, pos?: position) {
if (file !== '') {
const items = [
{
@@ -132,11 +133,22 @@ export default function SourceCode() {
}
}
+ const externalEditorTitle =
+ 'Open the source file in an external editor.\nA Ctrl-click '
+ + 'in the source code opens the editor at the selected location.'
+ + '\nThe editor used can be configured in Ivette settings.';
+
// Building the React component.
return (
<>
<TitleBar>
- <Code title={file}>{filename}</Code>
+ <IconButton
+ icon="DUPLICATE"
+ visible={file !== ''}
+ onClick={launchEditor}
+ title={externalEditorTitle}
+ />
+ <Code title={file} style={{ padding: '5px' }}>{filename}</Code>
<Hfill />
{themeButtons}
</TitleBar>
--
GitLab