Skip to content

Fix syntax highlighting in the trace explorer #36

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
VojtechStep wants to merge 3 commits into from
Closed

Fix syntax highlighting in the trace explorer #36

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a97c8f5
Fix retrieving a highlighter
VojtechStep Jul 16, 2026
72fafac
Add unstyled fallback to syntax highlighting
VojtechStep Jul 16, 2026
c604816
Fix performace of syntax highlighting in the trace explorer
VojtechStep Jul 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 31 additions & 6 deletions media/main.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 = '<pre class="shiki" style="background-color: var(--shiki-color-background)"><span class="line"><span style="color: var(--shiki-color-text)">' + window.inbox[i].goal_text + '</span></span></pre>';

Expand All @@ -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 = '<pre class="shiki" style="background-color: var(--shiki-color-background)"><span class="line"><span style="color: var(--shiki-color-text)">' + window.inbox[i].goal_text_elided + '</span></span></pre>';

// /////////////////////////////////////////////////////////////////////////////
}

if (window.enable_highlighting)
vscode.postMessage({
command: 'flush_highlight'
});


// /////////////////////////////////////////////////////////////////////////////

$('#message-feed').removeClass('is-hidden');
Expand Down
48 changes: 28 additions & 20 deletions src/provider.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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({
Expand All @@ -123,36 +123,44 @@ 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 'flush_highlight':
{
if (this._view)
this._view.webview.postMessage({
type: 'flush_highlight'
})
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':
Expand Down