[goals] Enable find widget in goal panel

Fixes #305 Signed-off-by: Ali Caglayan <alizter@gmail.com>
ejgallego · Feb 9, 2023 · 4103738 · 4103738
1 parent 71980e8
commit 4103738
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/CHANGES.md b/CHANGES.md
@@ -32,6 +32,7 @@
    user-configurable (by default 150) (@ejgallego, #303)
  - Coq Markdown files (.mv extension) are now highlighted properly
    using both Coq and Markdown syntax rules (@4ever2, #307)
+ - Goal view now supports find (@Alizter, #309, closes #305)
 
 # coq-lsp 0.1.4: View
 ---------------------

diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
@@ -31,7 +31,7 @@ export class InfoPanel {
   }
 
   panelFactory() {
-    let webviewOpts: WebviewOptions = { enableScripts: true };
+    let webviewOpts = { enableScripts: true, enableFindWidget: true };
     this.panel = window.createWebviewPanel(
       "goals",
       "Goals",