--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts Sun Oct 26 19:14:08 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts Sun Oct 26 19:17:30 2025 +0100
@@ -3,17 +3,17 @@
Isabelle sledgehammer panel as web view.
*/
-import { WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext, CancellationToken, window, Webview, Selection, Range, TextDocument, TextDocumentContentChangeEvent } from 'vscode';
-import * as path from 'path';
-import { text_colors } from './decorations';
-import * as vscode_lib from './vscode_lib'
-import * as lsp from './lsp';
-import { LanguageClient } from 'vscode-languageclient/node';
-import { Position } from 'vscode';
+import { WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext, CancellationToken, window, Webview, Selection, Range, TextDocument, TextDocumentContentChangeEvent } from "vscode";
+import * as path from "path";
+import { text_colors } from "./decorations";
+import * as vscode_lib from "./vscode_lib"
+import * as lsp from "./lsp";
+import { LanguageClient } from "vscode-languageclient/node";
+import { Position } from "vscode";
class Sledgehammer_Panel_Provider implements WebviewViewProvider {
- public static readonly view_type = 'isabelle-sledgehammer';
+ public static readonly view_type = "isabelle-sledgehammer";
private _view?: WebviewView;
private _lastResultPosition?: { uri: string; line: number; character: number; lineText: string };
private text_to_insert: string;
@@ -53,7 +53,7 @@
});
}
switch (message.command) {
- case 'apply':
+ case "apply":
this._language_client.sendNotification(lsp.sledgehammer_request_type, {
provers: message.provers,
isar: message.isar,
@@ -62,10 +62,10 @@
});
break;
- case 'cancel':
+ case "cancel":
this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
break;
- case 'locate':
+ case "locate":
this._language_client.sendNotification(lsp.sledgehammer_request_type, {
provers: message.provers,
isar: message.isar,
@@ -74,7 +74,7 @@
});
break;
- case 'insert_text':
+ case "insert_text":
this._language_client.sendNotification(lsp.sledgehammer_request_type, {
provers: message.provers,
isar: message.isar,
@@ -89,13 +89,13 @@
public updateStatus(message: string): void {
if (this._view) {
- this._view.webview.postMessage({ command: 'status', message });
+ this._view.webview.postMessage({ command: "status", message });
}
}
public update_provers(provers: string): void {
if (this._view) {
- this._view.webview.postMessage({ command: 'provers', provers });
+ this._view.webview.postMessage({ command: "provers", provers });
}
}
@@ -119,7 +119,7 @@
const pos = new Position(position.line, position.character);
const existingLineText = editor.document.lineAt(pos.line).text;
- const textToInsert = existingLineText.trim() === '' ? this.text_to_insert : '\n' + this.text_to_insert;
+ const textToInsert = existingLineText.trim() === "" ? this.text_to_insert : "\n" + this.text_to_insert;
editor.edit(editBuilder => {
editBuilder.insert(pos, textToInsert);
@@ -137,7 +137,7 @@
if (this._view) {
this._view.webview.postMessage({
- command: 'result',
+ command: "result",
content: result.content,
position: result.position,
sendback_id: result.sendback_id
@@ -148,14 +148,14 @@
public updateNoProver(provers: lsp.SledgehammerNoSuchProver): void {
if (this._view) {
- this._view.webview.postMessage({ command: 'no_provers' });
+ this._view.webview.postMessage({ command: "no_provers" });
}
}
public updateNoProofContext(): void {
if (this._view) {
- this._view.webview.postMessage({ command: 'no_proof_context' });
+ this._view.webview.postMessage({ command: "no_proof_context" });
}
}
@@ -165,10 +165,10 @@
}
function get_webview_html(webview: Webview | undefined, extension_path: string): string {
- const script_uri = webview?.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'sledgehammer.js')));
- const css_uri = webview?.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'sledgehammer.css')));
+ const script_uri = webview?.asWebviewUri(Uri.file(path.join(extension_path, "media", "sledgehammer.js")));
+ const css_uri = webview?.asWebviewUri(Uri.file(path.join(extension_path, "media", "sledgehammer.css")));
const font_uri =
- webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
+ webview.asWebviewUri(Uri.file(path.join(extension_path, "fonts", "IsabelleDejaVuSansMono.ttf")))
return `