From 18c0b3701d3e43005ec817d64f43622157650e49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= <marussy@mit.bme.hu>
Date: Sun, 15 Dec 2024 22:16:00 +0100
Subject: [PATCH] feat(frontend): go to definition in toolbar

---
 subprojects/frontend/src/editor/EditorButtons.tsx    | 10 ++++++++++
 subprojects/frontend/src/editor/EditorStore.ts       |  3 ++-
 subprojects/frontend/src/editor/createEditorState.ts |  4 ++++
 subprojects/frontend/src/xtext/OccurrencesService.ts |  2 +-
 subprojects/frontend/src/xtext/XtextClient.ts        |  2 +-
 5 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/subprojects/frontend/src/editor/EditorButtons.tsx b/subprojects/frontend/src/editor/EditorButtons.tsx
index 15f0f635..690e6a8d 100644
--- a/subprojects/frontend/src/editor/EditorButtons.tsx
+++ b/subprojects/frontend/src/editor/EditorButtons.tsx
@@ -16,6 +16,7 @@ import RedoIcon from '@mui/icons-material/Redo';
 import SaveIcon from '@mui/icons-material/Save';
 import SaveAsIcon from '@mui/icons-material/SaveAs';
 import SearchIcon from '@mui/icons-material/Search';
+import ShortcutIcon from '@mui/icons-material/ShortcutOutlined';
 import UndoIcon from '@mui/icons-material/Undo';
 import WarningIcon from '@mui/icons-material/Warning';
 import IconButton from '@mui/material/IconButton';
@@ -150,6 +151,15 @@ export default observer(function EditorButtons({
           </ToggleButton>
         </MuiTooltip>
       </ToggleButtonGroup>
+      <Tooltip title="Go to definition">
+        <IconButton
+          disabled={!editorStore?.opened}
+          onClick={() => editorStore?.goToDefinition()}
+          color="inherit"
+        >
+          <ShortcutIcon fontSize="small" />
+        </IconButton>
+      </Tooltip>
       <Tooltip title="Automatic format">
         <IconButton
           disabled={!editorStore?.opened}
diff --git a/subprojects/frontend/src/editor/EditorStore.ts b/subprojects/frontend/src/editor/EditorStore.ts
index a4460271..946d6534 100644
--- a/subprojects/frontend/src/editor/EditorStore.ts
+++ b/subprojects/frontend/src/editor/EditorStore.ts
@@ -351,8 +351,9 @@ export default class EditorStore {
     return this.client.hoverTooltip(pos);
   }
 
-  goToDefinition(pos: number): void {
+  goToDefinition(pos?: number): boolean {
     this.client?.goToDefinition(pos);
+    return true;
   }
 
   /**
diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts
index aac407e4..1f3fb306 100644
--- a/subprojects/frontend/src/editor/createEditorState.ts
+++ b/subprojects/frontend/src/editor/createEditorState.ts
@@ -142,6 +142,10 @@ export default function createEditorState(
         ...completionKeymap,
         ...foldKeymap,
         ...historyKeymap,
+        {
+          key: 'F3',
+          run: () => store.goToDefinition(),
+        },
         // Enable accepting completions with tab, overrides `Tab` from
         // `indentWithTab` if there is an active completion.
         { key: 'Tab', run: acceptCompletion },
diff --git a/subprojects/frontend/src/xtext/OccurrencesService.ts b/subprojects/frontend/src/xtext/OccurrencesService.ts
index 03858605..ce6d4fcf 100644
--- a/subprojects/frontend/src/xtext/OccurrencesService.ts
+++ b/subprojects/frontend/src/xtext/OccurrencesService.ts
@@ -144,7 +144,7 @@ export default class OccurrencesService {
     this.store.updateOccurrences(write, read, goToFirst, pos);
   }
 
-  goToDefinition(pos: number): Promise<void> {
+  goToDefinition(pos?: number): Promise<void> {
     return this.updateOccurrences(pos, true);
   }
 }
diff --git a/subprojects/frontend/src/xtext/XtextClient.ts b/subprojects/frontend/src/xtext/XtextClient.ts
index 26fe1cc2..1dd87e0c 100644
--- a/subprojects/frontend/src/xtext/XtextClient.ts
+++ b/subprojects/frontend/src/xtext/XtextClient.ts
@@ -165,7 +165,7 @@ export default class XtextClient {
     return this.hoverService.hoverTooltip(pos);
   }
 
-  goToDefinition(pos: number): void {
+  goToDefinition(pos?: number): void {
     this.occurrencesService.goToDefinition(pos).catch((e) => {
       log.error('Error while fetching occurrences', e);
     });