From ddcef74f088c74530aba1f261f669eb415b42bb7 Mon Sep 17 00:00:00 2001 From: Fred Sauer Date: Mon, 30 Mar 2026 18:30:38 -0700 Subject: [PATCH] Delete unused highlightSearch in ui.ts --- src/ide/ui.ts | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/ide/ui.ts b/src/ide/ui.ts index 3afc3c0f..c22e3afb 100644 --- a/src/ide/ui.ts +++ b/src/ide/ui.ts @@ -2323,15 +2323,6 @@ function writeOutputROMFile() { alternateLocalFilesystem.setFileData(`bin/${prefix}${suffix}`, current_output); } } -export function highlightSearch(query: string) { // TODO: filename? - var wnd = projectWindows.getActive(); - if (wnd instanceof SourceEditor) { - var sc = wnd.editor.getSearchCursor(query); - if (sc.findNext()) { - wnd.editor.setSelection(sc.pos.to, sc.pos.from); - } - } -} function startUIWhenVisible() { let started = false;