From 1781a9354c7c305a5ccbf0f69778bf76a0568a2d Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Thu, 23 Jul 2026 15:05:50 +0200 Subject: [PATCH] Remove remnants of old syntax highlighting --- media/main.js | 39 +++++++++++++------------------- src/provider.ts | 60 ------------------------------------------------- 2 files changed, 16 insertions(+), 83 deletions(-) diff --git a/media/main.js b/media/main.js index fc5ebd9..b102c44 100644 --- a/media/main.js +++ b/media/main.js @@ -9,17 +9,6 @@ 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; - case 'highlight_inline': - $('#' + message.id).html(message.html); - break; case 'trace': clear(); trace(message.trace); @@ -648,7 +637,7 @@ ${step.value.findall_solution_text}
- 
${step.value.suspend_sibling.goal_text}
+ ${format_highlight_box(step.value.suspend_sibling.goal_text)}
@@ -697,7 +686,7 @@ ${step.value.findall_solution_text}
- 
${step.value[i].goal_text}
+ ${format_highlight_box(step.value[i].goal_text)}
`; } @@ -1057,7 +1046,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${rule_loc_file} (${r
- 
${rule_text_full}
+ ${format_highlight_box(rule_text_full)}
`; return fmt; @@ -1088,7 +1077,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${rule_loc_file} (${r
- 
${element[i].value}
+ ${format_highlight_box(element[i].value)}
`; } @@ -1138,7 +1127,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${rule_loc_file} (${r
- 
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
`; } else { @@ -1154,7 +1143,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${rule_loc_file} (${r
- 
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
`; } @@ -1197,7 +1186,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} ( ${elide(20, attempt_text)}
- 
${attempt_text}
+ ${format_highlight_box(attempt_text)}
`; return fmt; @@ -1244,7 +1233,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} (
- 
${element.chr_new_goals[i].goal_text}
+ ${format_highlight_box(element.chr_new_goals[i].goal_text)}
`; @@ -1285,7 +1274,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} (
- 
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
`; @@ -1333,7 +1322,7 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} (
- 
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
`; @@ -1348,6 +1337,10 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} ( return fmt; } + function format_highlight_box(text) { + return `
${text}
` + } + // ///////////////////////////////////////////////////////////////////////////// // // ///////////////////////////////////////////////////////////////////////////// @@ -1652,9 +1645,9 @@ class="has-tooltip-arrow has-tooltip-bottom" data-tooltip="${attempt_loc_file} ( window.inbox[i].goal_text_elided = elide(25, window.inbox[i].goal_text); - window.inbox[i].goal_text_highlighted = '
' + window.inbox[i].goal_text + '
'; + window.inbox[i].goal_text_highlighted = format_highlight_box(window.inbox[i].goal_text) - window.inbox[i].goal_text_highlighted_elided = '
' + window.inbox[i].goal_text_elided + '
'; + window.inbox[i].goal_text_highlighted_elided = format_highlight_box(window.inbox[i].goal_text_elided) // ///////////////////////////////////////////////////////////////////////////// } diff --git a/src/provider.ts b/src/provider.ts index 6f091d8..f674a9d 100644 --- a/src/provider.ts +++ b/src/provider.ts @@ -58,20 +58,6 @@ export class TraceProvider implements vscode.WebviewViewProvider { this._channel.appendLine("Running extension for " + os.platform() + " - " + os.release()); - let elpi_lang_grammar_path = vscode.Uri.joinPath(this._extensionUri, 'syntaxes', 'elpi.tmLanguage.json').path; - - if (os.platform().toString().toLowerCase() == "win32") - elpi_lang_grammar_path = elpi_lang_grammar_path.slice(1); - - this._channel.appendLine("Loading grammar file " + elpi_lang_grammar_path); - - const elpi_lang_grammer = JSON.parse(fs.readFileSync(elpi_lang_grammar_path, 'utf8')); - const elpi_lang = { - id: "elpi", - scopeName: 'source.elpi', - grammar: elpi_lang_grammer - }; - this._elpi = ""; this._elpi_trace_elaborator = ""; @@ -116,52 +102,6 @@ export class TraceProvider implements vscode.WebviewViewProvider { webviewView.webview.onDidReceiveMessage(message => { switch (message.command) { - - case 'highlight': - { - const code = message.value; - const indx = message.index; - let html = undefined; - - if (this._view) - this._view.webview.postMessage({ - type: 'highlight', - html: html, - indx: indx - }); - - break; - } - case 'highlight_elided': - { - const code = message.value; - const indx = message.index; - let html = undefined; - - 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._view) - this._view.webview.postMessage({ - type: 'highlight_inline', - html: html, - id: id - }); - - break; - } case 'notify': { vscode.window.showInformationMessage(message.value);