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)}
${step.value[i].goal_text}
+ ${format_highlight_box(step.value[i].goal_text)}
${rule_text_full}
+ ${format_highlight_box(rule_text_full)}
${element[i].value}
+ ${format_highlight_box(element[i].value)}
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
${attempt_text}
+ ${format_highlight_box(attempt_text)}
${element.chr_new_goals[i].goal_text}
+ ${format_highlight_box(element.chr_new_goals[i].goal_text)}
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
${element[i].goal_text}
+ ${format_highlight_box(element[i].goal_text)}
${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);