tuned quotes: follow Isabelle majority style, instead of JS/TS;
authorwenzelm
Sun, 26 Oct 2025 19:17:30 +0100
changeset 83402 3de9cda419e4
parent 83401 1d9b1ca7977e
child 83403 e22d2d321e50
tuned quotes: follow Isabelle majority style, instead of JS/TS;
src/Tools/VSCode/extension/src/sledgehammer_panel.ts
--- 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 `