chore: replace webview-ui-toolkit in abbreviationview

leanprover · Nov 5, 2024 · 1c39a21 · 1c39a21
1 parent cdd9fbb
commit 1c39a21
Show file tree

Hide file tree

Showing 6 changed files with 45 additions and 16 deletions.
diff --git a/package-lock.json b/package-lock.json
diff --git a/vscode-lean4/.vscodeignore b/vscode-lean4/.vscodeignore
@@ -14,6 +14,7 @@
 !dist/lean4-infoview/codicon.ttf
 !dist/loogleview/static
 !dist/moogleview/static
+!dist/abbreviationview/static
 !media
 !manual
 !images

diff --git a/vscode-lean4/abbreviationview/index.ts b/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)
+}
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -939,7 +939,6 @@
         "@leanprover/unicode-input": "~0.1.0",
         "@leanprover/unicode-input-component": "~0.1.0",
         "@vscode/codicons": "^0.0.36",
-        "@vscode/webview-ui-toolkit": "^1.4.0",
         "@vscode-elements/elements": "^1.7.1",
         "markdown-it": "^14.1.0",
         "markdown-it-anchor": "^9.0.1",

diff --git a/vscode-lean4/src/abbreviationview.ts b/vscode-lean4/src/abbreviationview.ts
@@ -52,10 +52,21 @@ export class AbbreviationView implements Disposable {
                 <meta charset="UTF-8" />
                 <meta http-equiv="Content-type" content="text/html;charset=utf-8">
                 <title>AbbreviationView</title>
+                <script
+                    src="${this.webviewUri(this.webviewPanel, 'dist', 'abbreviationview', 'static', 'elements', 'bundled.js')}"
+                    type="module"
+                ></script>
                 <script defer data-id="abbreviationview-script" src="${this.webviewUri(this.webviewPanel, 'dist/abbreviationview.js')}" abbreviations="${escapeHtml(JSON.stringify(abbreviations))}"></script>
             </head>
             <body>
-                <vscode-data-grid id="abbreviation-grid" aria-label="Abbreviations" grid-template-columns="20em 1fr"></vscode-data-grid>
+                <vscode-table aria-label="Abbreviations" responsive resizable bordered zebra>
+                    <vscode-table-header slot="header">
+                        <vscode-table-header-cell>Abbreviation</vscode-table-header-cell>
+                        <vscode-table-header-cell>Unicode symbol</vscode-table-header-cell>
+                    </vscode-table-header>
+                    <vscode-table-body id="abbreviation-table" slot="body">
+                    </vscode-table-body>
+                </vscode-table>
             </body>
             </html>`
         this.webviewPanel.reveal()

diff --git a/vscode-lean4/webpack.config.js b/vscode-lean4/webpack.config.js
@@ -177,6 +177,16 @@ const getAbbreviationViewConfig = env => ({
         filename: 'abbreviationview.js',
         path: path.resolve(__dirname, 'dist'),
     },
+    plugins: [
+        new CopyPlugin({
+            patterns: [
+                {
+                    from: '../node_modules/@vscode-elements/elements/dist',
+                    to: path.resolve(__dirname, 'dist', 'abbreviationview', 'static', 'elements'),
+                },
+            ],
+        }),
+    ],
 })
 
 /** @type {(env: Env) => import('webpack').Configuration} */