# HG changeset patch # User wenzelm # Date 1761502925 -3600 # Node ID 4c9ed0e60da20a0f9569b67f5a2a36467d643120 # Parent e22d2d321e50219c11b1259692151a74d7872871 tuned whitespace; diff -r e22d2d321e50 -r 4c9ed0e60da2 src/Tools/VSCode/extension/src/sledgehammer_panel.ts --- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts Sun Oct 26 19:20:03 2025 +0100 +++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts Sun Oct 26 19:22:05 2025 +0100 @@ -4,7 +4,8 @@ Control panel for Sledgehammer. */ -import { WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext, CancellationToken, window, Webview, Selection, Range, TextDocument, TextDocumentContentChangeEvent } 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" @@ -108,7 +109,7 @@ const position = new Position(state_location.line, state_location.character); editor.selections = [new Selection(position, position)]; editor.revealRange(new Range(position, position)); - } + } } public insert(position: { uri: string; line: number; character: number }): void { @@ -120,7 +121,8 @@ 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); @@ -143,7 +145,7 @@ position: result.position, sendback_id: result.sendback_id }); - + } } @@ -166,8 +168,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"))) @@ -185,7 +189,7 @@ src: url(${font_uri}); } ${_get_decorations()} - + Sledgehammer Panel