chore: replace webview-ui-toolkit (#545)

[`@vscode/webview-ui-toolkit` is being deprecated in
January](microsoft/vscode-webview-ui-toolkit#561).
This PR replaces the UI components from `@vscode/webview-ui-toolkit`
with components from `@vscode-elements/elements`.

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.7.7",
+    "version": "0.7.8",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -51,7 +51,7 @@
     "dependencies": {
         "@leanprover/infoview-api": "~0.4.0",
         "@vscode/codicons": "^0.0.32",
-        "@vscode/webview-ui-toolkit": "^1.4.0",
+        "@vscode-elements/react-elements": "^0.5.0",
         "es-module-shims": "^1.7.3",
         "react-fast-compare": "^3.2.2",
         "tachyons": "^4.12.0",

lean4-infoview/src/infoview/main.tsx

@@ -1,4 +1,4 @@
-import { VSCodeButton } from '@vscode/webview-ui-toolkit/react'
+import { VscodeButton } from '@vscode-elements/react-elements'
 import * as React from 'react'
 import * as ReactDOM from 'react-dom/client'
 import type { DidCloseTextDocumentParams, DocumentUri, Location } from 'vscode-languageserver-protocol'
@@ -85,13 +85,13 @@ function Main() {
                     </div>
                 )}
                 {curUri && (
-                    <VSCodeButton
+                    <VscodeButton
                         className="restart-file-button"
                         onClick={_ => ec.api.restartFile(curUri)}
                         title="Restarts this file, rebuilding all of its outdated dependencies."
                     >
                         Restart File
-                    </VSCodeButton>
+                    </VscodeButton>
                 )}
             </div>
         )

vscode-lean4/.vscodeignore

@@ -14,6 +14,7 @@
 !dist/lean4-infoview/codicon.ttf
 !dist/loogleview/static
 !dist/moogleview/static
+!dist/abbreviationview/static
 !media
 !manual
 !images

vscode-lean4/abbreviationview/index.ts

@@ -1,17 +1,16 @@
-import {
-    DataGrid,
-    provideVSCodeDesignSystem,
-    vsCodeDataGrid,
-    vsCodeDataGridCell,
-    vsCodeDataGridRow,
-} from '@vscode/webview-ui-toolkit'
-
-provideVSCodeDesignSystem().register(vsCodeDataGrid(), vsCodeDataGridRow(), vsCodeDataGridCell())
-
-const abbreviations: { Abbreviation: string; 'Unicode symbol': string } = JSON.parse(
+const abbreviations: { Abbreviation: string; 'Unicode symbol': string }[] = JSON.parse(
     document.querySelector('script[data-id="abbreviationview-script"]')!.getAttribute('abbreviations')!,
 )
 
-const grid = document.getElementById('abbreviation-grid')! as DataGrid
+const tableBody = document.getElementById('abbreviation-table')!
 
-grid.rowsData = abbreviations as any
+for (const { Abbreviation: abbr, 'Unicode symbol': symb } of abbreviations) {
+    const row = document.createElement('vscode-table-row')
+    const abbrCell = document.createElement('vscode-table-cell')
+    abbrCell.innerText = abbr
+    row.appendChild(abbrCell)
+    const symbCell = document.createElement('vscode-table-cell')
+    symbCell.innerText = symb
+    row.appendChild(symbCell)
+    tableBody.appendChild(row)
+}

vscode-lean4/loogleview/index.ts

@@ -1,8 +1,5 @@
 import { AbbreviationConfig } from '@leanprover/unicode-input'
 import { InputAbbreviationRewriter } from '@leanprover/unicode-input-component'
-import { provideVSCodeDesignSystem, vsCodeButton, vsCodeLink, vsCodeTextField } from '@vscode/webview-ui-toolkit'
-
-provideVSCodeDesignSystem().register(vsCodeButton(), vsCodeTextField(), vsCodeLink())
 
 const vscodeApi = acquireVsCodeApi()
 
@@ -135,7 +132,7 @@ class LoogleView {
         })
 
         for (const querySuggestionElement of view.staticSuggestions) {
-            if (!(querySuggestionElement instanceof HTMLElement) || querySuggestionElement.tagName !== 'VSCODE-LINK') {
+            if (!(querySuggestionElement instanceof HTMLElement) || querySuggestionElement.tagName !== 'A') {
                 continue
             }
             const querySuggestion = querySuggestionElement.innerText
@@ -203,7 +200,8 @@ class LoogleView {
     }
 
     private createQuerySuggestionNode(querySuggestion: string): HTMLElement {
-        const link = document.createElement('vscode-link')
+        const link = document.createElement('a')
+        link.href = 'javascript:void(0)'
         link.innerText = querySuggestion
         link.addEventListener('click', () => this.runSuggestion(querySuggestion))
         return link
@@ -212,7 +210,7 @@ class LoogleView {
     private createHitNameNode(name: string, module: string): HTMLElement {
         // This is not correct (consider e.g. escaped dots in french quotes) but it should be good enough for now.
         const docUrl = `https://leanprover-community.github.io/mathlib4_docs/${encodeURIComponent(module.replace(new RegExp(/\./, 'g'), '/'))}.html#${encodeURIComponent(name)}`
-        const link = document.createElement('vscode-link')
+        const link = document.createElement('a')
         link.innerText = name
         link.setAttribute('href', `command:simpleBrowser.show?${encodeURIComponent(JSON.stringify([docUrl]))}`)
         return link
@@ -232,12 +230,12 @@ class LoogleView {
         this.resultHeader.hidden = hits.length === 0
         const resultNodes = hits.map(hit => {
             const entry = document.createElement('li')
-            const identifierNode = document.createElement('span')
-            identifierNode.appendChild(this.createHitNameNode(hit.name, hit.module))
-            identifierNode.appendChild(document.createTextNode(` @ ${hit.module}`))
-            entry.appendChild(identifierNode)
-            entry.appendChild(document.createElement('br'))
-            entry.appendChild(document.createTextNode(hit.type))
+            const paragraph = document.createElement('p')
+            paragraph.appendChild(this.createHitNameNode(hit.name, hit.module))
+            paragraph.appendChild(document.createTextNode(` @ ${hit.module}`))
+            paragraph.appendChild(document.createElement('br'))
+            paragraph.appendChild(document.createTextNode(hit.type))
+            entry.appendChild(paragraph)
             return entry
         })
         this.results.replaceChildren(...resultNodes)