diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx index d13ec304fc641ef02914b84495fc512bcff21542..8582d0b50059c08e706a4ab2498344040be99998 100644 --- a/ivette/src/renderer/Application.tsx +++ b/ivette/src/renderer/Application.tsx @@ -19,7 +19,7 @@ import * as Controller from './Controller'; import ASTview from './ASTview'; import ASTinfo from './ASTinfo'; -import Globals from './Globals'; +import Globals, { GlobalHint, useHints } from './Globals'; import Properties from './Properties'; import Locations from './Locations'; import Values from './Values'; @@ -61,6 +61,14 @@ export default (() => { Dome.useFlipSettings('frama-c.sidebar.unfold', true); const [viewbar, flipViewbar] = Dome.useFlipSettings('frama-c.viewbar.unfold', true); + const [hints, onSearchHint] = useHints(); + const [, setSelection] = States.useSelection(); + const onGlobalHint = (h: GlobalHint) => { + setSelection({ location: h.value }); + }; + const onSelectHint = () => { + if (hints.length === 1) onGlobalHint(hints[0]); + }; return ( <Vfill> @@ -74,7 +82,13 @@ export default (() => { <Controller.Control /> <HistorySelectionControls /> <Toolbar.Filler /> - <Toolbar.SearchField placeholder="Search…" /> + <Toolbar.SearchField + placeholder="Search…" + hints={hints} + onSearch={onSearchHint} + onSelect={onSelectHint} + onHint={onGlobalHint} + /> <Toolbar.Button icon="ITEMS.GRID" title="Customize Main View" diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx index 316ab76d28234bb4ffc675d244710bd3bb4c717f..4b153c03dde17807d64943188e5a4667c6a0e063 100644 --- a/ivette/src/renderer/Globals.tsx +++ b/ivette/src/renderer/Globals.tsx @@ -4,12 +4,41 @@ import React from 'react'; import { Section, Item } from 'dome/frame/sidebars'; +import type { Hint } from 'dome/frame/toolbars'; import * as States from 'frama-c/states'; import { alpha } from 'dome/data/compare'; import { functions, functionsData } from 'frama-c/api/kernel/ast'; // -------------------------------------------------------------------------- -// --- Globals Section +// --- Global Search Hints +// -------------------------------------------------------------------------- + +export type GlobalHint = Hint<States.Location>; + +const makeHint = (fct: functionsData): GlobalHint => ({ + id: fct.key, + label: fct.name, + title: fct.signature, + value: { function: fct.name }, +}); + +export function useHints(): [GlobalHint[], (pattern: string) => void] { + const fcts = States.useSyncArray(functions).getArray(); + const [hints, setHints] = React.useState<GlobalHint[]>([]); + const onSearch = (pattern: string) => { + if (pattern === '') setHints([]); + else { + const p = pattern.toLowerCase(); + setHints(fcts.filter((fn) => ( + 0 <= fn.name.toLowerCase().indexOf(p) + )).map(makeHint)); + } + }; + return [hints, onSearch]; +} + +// -------------------------------------------------------------------------- +// --- Globals Section(s) // -------------------------------------------------------------------------- export default () => {