From a97c8f58239fafb4b03db274aa01b24aa3fce948 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Thu, 16 Jul 2026 16:39:45 +0200 Subject: [PATCH 1/3] Fix retrieving a highlighter Removing shiki's built-in language grammars lead to it failing to initialize, so syntax highlighting in the trace explorer never worked. This is fixed by passing it the elpi grammar during initialization --- src/provider.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/provider.ts b/src/provider.ts index 5b894d0..82962fa 100644 --- a/src/provider.ts +++ b/src/provider.ts @@ -70,10 +70,10 @@ export class TraceProvider implements vscode.WebviewViewProvider { this._watcher_target = this._target_dir + "traced.tmp.json"; this._watcher_target_elaborated = this._target_dir + "traced.json"; - shiki.getHighlighter({theme: 'css-variables'}).then(highlighter => { - this._highlighter = highlighter; - this._highlighter.loadLanguage(elpi_lang); - }); + shiki.getHighlighter({theme: 'css-variables', langs: [elpi_lang]}) + .then(highlighter => { + this._highlighter = highlighter; + }); if (os.platform().toString().toLowerCase() == "win32") this._cat = "type"; From 72fafac9048f2dae1abd8952cae8b4e3ffea59ae Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Thu, 16 Jul 2026 16:41:31 +0200 Subject: [PATCH 2/3] Add unstyled fallback to syntax highlighting --- src/provider.ts | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/provider.ts b/src/provider.ts index 82962fa..4fd64f9 100644 --- a/src/provider.ts +++ b/src/provider.ts @@ -105,10 +105,10 @@ export class TraceProvider implements vscode.WebviewViewProvider { { const code = message.value; const indx = message.index; - let html = undefined; - - if (this._highlighter) - html = this._highlighter.codeToHtml(code, { lang: 'elpi' }); + const html = + this._highlighter + ? this._highlighter.codeToHtml(code, { lang: 'elpi' }) + : code; if (this._view) this._view.webview.postMessage({ @@ -123,36 +123,36 @@ export class TraceProvider implements vscode.WebviewViewProvider { { const code = message.value; const indx = message.index; - let html = undefined; - - if (this._highlighter) - html = this._highlighter.codeToHtml(code, { lang: 'elpi' }); - + const html = + this._highlighter + ? this._highlighter.codeToHtml(code, { lang: 'elpi' }) + : code; + if (this._view) this._view.webview.postMessage({ type: 'highlight_elided', html: html, indx: indx }); - + break; } case 'highlight_inline': { const code = message.value; const id = message.id; - let html = undefined; - - if (this._highlighter) - html = this._highlighter.codeToHtml(code, { lang: 'elpi' }); - + const html = + this._highlighter + ? this._highlighter.codeToHtml(code, { lang: 'elpi' }) + : code; + if (this._view) this._view.webview.postMessage({ type: 'highlight_inline', html: html, id: id }); - + break; } case 'notify': From c604816bec19e2482c80dff94fd79007b2068639 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Thu, 16 Jul 2026 16:43:25 +0200 Subject: [PATCH 3/3] Fix performace of syntax highlighting in the trace explorer The terrible performance was caused by not batching the redrawing of cards when the syntax information was updated. This is because each card's highlighting info was passed in a separate message, which are processed in different ticks, so every card caused a redraw. Here we add manual batching, so that the cards are all updated in the same tick. --- media/main.js | 37 +++++++++++++++++++++++++++++++------ src/provider.ts | 8 ++++++++ 2 files changed, 39 insertions(+), 6 deletions(-) diff --git a/media/main.js b/media/main.js index fd9379d..16a8817 100644 --- a/media/main.js +++ b/media/main.js @@ -5,18 +5,35 @@ const oldState = vscode.getState(); + let highlight_queue = []; + // Handle messages sent from the extension to the webview window.addEventListener('message', event => { const message = event.data; // The json data that the extension sent switch (message.type) { case 'highlight': - // console.log('Got', message.html, 'for', message.indx); - window.inbox[message.indx].goal_text_highlighted = message.html; - break; case 'highlight_elided': - // console.log('Got', message.html, 'for', message.indx); - window.inbox[message.indx].goal_text_highlighted_elided = message.html; - break; + // Batch highlighting requests; since the highlight information + // is passed through a MessagePort, we can't take advantage of Vue's + // automatic batching, because the messages won't be processed in the same + // tick + highlight_queue.push(message) + break; + case 'flush_highlight': { + let msg; + while (typeof (msg = highlight_queue.shift()) !== 'undefined') { + switch (msg.type) { + case 'highlight': + window.inbox[msg.indx].goal_text_highlighted = msg.html; + break; + case 'highlight_elided': + window.inbox[msg.indx].goal_text_highlighted_elided = msg.html; + break; + default: + break; + } + } + } case 'highlight_inline': $('#' + message.id).html(message.html); break; @@ -1701,6 +1718,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} ( index: i, value: window.inbox[i].goal_text }); + else window.inbox[i].goal_text_highlighted = '
' + window.inbox[i].goal_text + '
'; @@ -1710,12 +1728,19 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} ( index: i, value: window.inbox[i].goal_text_elided }); + else window.inbox[i].goal_text_highlighted_elided = '
' + window.inbox[i].goal_text_elided + '
'; // ///////////////////////////////////////////////////////////////////////////// } + if (window.enable_highlighting) + vscode.postMessage({ + command: 'flush_highlight' + }); + + // ///////////////////////////////////////////////////////////////////////////// $('#message-feed').removeClass('is-hidden'); diff --git a/src/provider.ts b/src/provider.ts index 4fd64f9..7e02dd4 100644 --- a/src/provider.ts +++ b/src/provider.ts @@ -137,6 +137,14 @@ export class TraceProvider implements vscode.WebviewViewProvider { break; } + case 'flush_highlight': + { + if (this._view) + this._view.webview.postMessage({ + type: 'flush_highlight' + }) + break; + } case 'highlight_inline': { const code = message.value;