From 481334fc952e24a1c2261e685067cd90888f5dde Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 2 Mar 2023 14:01:25 +0100
Subject: [PATCH] [Ivette] SourceCode: adds documentation of useful shortcuts.
---
ivette/src/frama-c/kernel/SourceCode.tsx | 30 ++++++++++++++++++++----
1 file changed, 25 insertions(+), 5 deletions(-)
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index 59f285f981d..2ede47f2e64 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -25,11 +25,12 @@ import * as Path from 'path';
import * as Dome from 'dome';
import * as System from 'dome/system';
-import * as Boxes from 'dome/layout/boxes';
import * as Editor from 'dome/text/editor';
import * as Labels from 'dome/controls/labels';
import * as Settings from 'dome/data/settings';
import * as Buttons from 'dome/controls/buttons';
+import * as Dialogs from 'dome/dialogs';
+import * as Toolbars from 'dome/frame/toolbars';
import { Selection, Document } from 'dome/text/editor';
@@ -265,9 +266,22 @@ export default function SourceCode(): JSX.Element {
React.useEffect(() => Locations.set(view, { ivette: loc }), [view, loc]);
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.';
+ 'Open the source file in an external editor.';
+
+ const shortcuts =
+ 'Ctrl+click: open file in an external editor at the selected location.\n'
+ + 'Alt+f: search for text or regexp.\n'
+ + 'Alt+g: go to line.';
+
+ const shortcutsTitle = 'Useful shortcuts:\n' + shortcuts;
+
+ async function displayShortcuts(): Promise<void> {
+ await Dialogs.showMessageBox({
+ buttons: [{label:"Ok"}],
+ details: shortcuts,
+ message: 'Useful shortcuts'
+ });
+ }
return (
<>
@@ -279,7 +293,13 @@ export default function SourceCode(): JSX.Element {
title={externalEditorTitle}
/>
<Labels.Code title={file}>{filename}</Labels.Code>
- <Boxes.Hfill />
+ <Toolbars.Filler />
+ <Buttons.IconButton
+ icon="HELP"
+ onClick={displayShortcuts}
+ title={shortcutsTitle}
+ />
+ <Toolbars.Inset/>
</Ivette.TitleBar>
<Component style={{ fontSize: `${fontSize}px` }} />
</>
--
GitLab