misc tuning: avoid camel-case;
authorwenzelm
Sat, 01 Nov 2025 14:51:26 +0100
changeset 83442 3a679f0ad4b3
parent 83441 37628234a530
child 83443 5149c50d46cc
misc tuning: avoid camel-case;
src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sat Nov 01 14:36:09 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sat Nov 01 14:51:26 2025 +0100
@@ -17,7 +17,7 @@
 class Sledgehammer_Panel_Provider implements WebviewViewProvider {
   public static readonly view_type = "isabelle-sledgehammer";
   private _view?: WebviewView;
-  private _lastResultPosition?: { uri: string; line: number; character: number; lineText: string };
+  private _result_position?: { uri: string; line: number; character: number; line_text: string };
   private text_to_insert: string;
 
   constructor(
@@ -89,10 +89,10 @@
   }
 
   public locate(state_location: { uri: string; line: number; character: number }): void {
-    const docUri = Uri.parse(state_location.uri);
+    const doc_uri = Uri.parse(state_location.uri);
     const editor = window.activeTextEditor;
 
-    if (editor && editor.document.uri.toString() === docUri.toString()) {
+    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)];
       editor.revealRange(new Range(position, position));
@@ -111,19 +111,14 @@
     const textToInsert =
       existingLineText.trim() === "" ? this.text_to_insert : "\n" + this.text_to_insert;
 
-    editor.edit(editBuilder => {
-      editBuilder.insert(pos, textToInsert);
-    });
+    editor.edit(edit_builder => edit_builder.insert(pos, textToInsert));
   }
 
 
   public update_output(result: lsp.Sledgehammer_Output): void {
     const editor = window.activeTextEditor;
-    const lineText = editor?.document.lineAt(result.position.line).text ?? "";
-    this._lastResultPosition = {
-      ...result.position,
-      lineText
-    };
+    const line_text = editor?.document.lineAt(result.position.line).text ?? "";
+    this._result_position = { ...result.position, line_text };
 
     if (this._view) {
         this._view.webview.postMessage({