# HG changeset patch
# User wenzelm
# Date 1762005602 -3600
# Node ID 5149c50d46cc34760caf4b5e47e0268e166af221
# Parent  3a679f0ad4b304cff8d28672296abf667f1f3172
misc tuning;

diff -r 3a679f0ad4b3 -r 5149c50d46cc src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sat Nov 01 14:51:26 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sat Nov 01 15:00:02 2025 +0100
@@ -25,7 +25,11 @@
     private readonly _language_client: LanguageClient
   ) { }
 
-  public resolveWebviewView(view: WebviewView, context: WebviewViewResolveContext, _token: CancellationToken): void {
+  public resolveWebviewView(
+    view: WebviewView,
+    context: WebviewViewResolveContext,
+    _token: CancellationToken
+  ): void {
     this._view = view;
     this._view.webview.options = {
       enableScripts: true,
@@ -42,38 +46,38 @@
   }
 
   private _setup_message_handler(): void {
-    if (!this._view) return;
-    this._view.webview.onDidReceiveMessage(async message => {
-      const editor = window.activeTextEditor;
-      const pos = editor?.selection.active;
-
-      if (editor && pos) {
-        this._language_client.sendNotification(lsp.caret_update_type, {
-          uri: editor.document.uri.toString(),
-          line: pos.line,
-          character: pos.character
-        });
-      }
-      switch (message.command) {
-        case "apply":
-          this._language_client.sendNotification(lsp.sledgehammer_request_type, {
-            provers: message.provers,
-            isar: message.isar,
-            try0: message.try0
+    if (this._view) {
+      this._view.webview.onDidReceiveMessage(async message => {
+        const editor = window.activeTextEditor;
+        const pos = editor?.selection.active;
+        if (editor && pos) {
+          this._language_client.sendNotification(lsp.caret_update_type, {
+            uri: editor.document.uri.toString(),
+            line: pos.line,
+            character: pos.character
           });
-          break;
-        case "cancel":
-          this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
-          break;
-        case "locate":
-          this._language_client.sendNotification(lsp.sledgehammer_locate_type);
-          break;
-        case "insert":
-          this._language_client.sendNotification(lsp.sledgehammer_insert_type);
-          this.text_to_insert = message.text;
-          break;
-      }
-    });
+        }
+        switch (message.command) {
+          case "apply":
+            this._language_client.sendNotification(lsp.sledgehammer_request_type, {
+              provers: message.provers,
+              isar: message.isar,
+              try0: message.try0
+            });
+            break;
+          case "cancel":
+            this._language_client.sendNotification(lsp.sledgehammer_cancel_type);
+            break;
+          case "locate":
+            this._language_client.sendNotification(lsp.sledgehammer_locate_type);
+            break;
+          case "insert":
+            this._language_client.sendNotification(lsp.sledgehammer_insert_type);
+            this.text_to_insert = message.text;
+            break;
+        }
+      });
+    }
   }
 
   public update_status(message: string): void {
@@ -91,7 +95,6 @@
   public locate(state_location: { uri: string; line: number; character: number }): void {
     const doc_uri = Uri.parse(state_location.uri);
     const editor = window.activeTextEditor;
-
     if (editor && editor.document.uri.toString() === doc_uri.toString()) {
       const position = new Position(state_location.line, state_location.character);
       editor.selections = [new Selection(position, position)];
@@ -101,33 +104,29 @@
 
   public insert(position: { uri: string; line: number; character: number }): void {
     const editor = window.activeTextEditor;
-    if (!editor) return;
-
-    const uri = Uri.parse(position.uri);
-    if (editor.document.uri.toString() !== uri.toString()) return;
-
-    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;
-
-    editor.edit(edit_builder => edit_builder.insert(pos, textToInsert));
+    if (editor) {
+      const uri = Uri.parse(position.uri);
+      if (editor.document.uri.toString() === uri.toString()) {
+        const pos = new Position(position.line, position.character);
+        const line_text = editor.document.lineAt(pos.line).text;
+        const text_to_insert =
+          line_text.trim() === "" ? this.text_to_insert : "\n" + this.text_to_insert;
+        editor.edit(edit_builder => edit_builder.insert(pos, text_to_insert));
+      }
+    }
   }
 
-
   public update_output(result: lsp.Sledgehammer_Output): void {
     const editor = window.activeTextEditor;
     const line_text = editor?.document.lineAt(result.position.line).text ?? "";
     this._result_position = { ...result.position, line_text };
-
     if (this._view) {
-        this._view.webview.postMessage({
-          command: "result",
-          content: result.content,
-          position: result.position,
-          sendback_id: result.sendback_id
-        });
-
+      this._view.webview.postMessage({
+        command: "result",
+        content: result.content,
+        position: result.position,
+        sendback_id: result.sendback_id
+      });
     }
   }
 
@@ -150,7 +149,6 @@
   const font_uri =
     webview.asWebviewUri(Uri.file(path.join(extension_path, "fonts", "IsabelleDejaVuSansMono.ttf")))
 
-
   return `
     <!DOCTYPE html>
     <html lang="en">