tuned signature;
authorwenzelm
Fri, 11 Mar 2022 13:17:14 +0100
changeset 75264 5cae3e486cec
parent 75263 0a440e255a64
child 75265 481665cc17e6
tuned signature;
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/vscode_lib.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Mar 11 13:07:06 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Mar 11 13:17:14 2022 +0100
@@ -45,9 +45,9 @@
 
     const language_client_options: LanguageClientOptions = {
       documentSelector: [
-        { language: "isabelle", scheme: "file" },
-        { language: "isabelle-ml", scheme: "file" },
-        { language: "bibtex", scheme: "file" }
+        { language: "isabelle", scheme: vscode_lib.file_scheme },
+        { language: "isabelle-ml", scheme: vscode_lib.file_scheme },
+        { language: "bibtex", scheme: vscode_lib.file_scheme }
       ]
     }
 
--- a/src/Tools/VSCode/extension/src/vscode_lib.ts	Fri Mar 11 13:07:06 2022 +0100
+++ b/src/Tools/VSCode/extension/src/vscode_lib.ts	Fri Mar 11 13:17:14 2022 +0100
@@ -8,9 +8,11 @@
 
 /* files */
 
+export const file_scheme: string = "file"
+
 export function is_file(uri: Uri): boolean
 {
-  return uri.scheme === "file"
+  return uri.scheme === file_scheme
 }
 
 export function find_file_editor(uri: Uri): TextEditor | undefined