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 = '<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>';
 
@@ -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');
diff --git a/src/provider.ts b/src/provider.ts
index 5b894d0..7e02dd4 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";
@@ -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,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':