more robust startup wrt. VSCode workspace (by Fabian Huch);
authorwenzelm
Tue, 22 Feb 2022 12:23:21 +0100
changeset 75127 1fed80019bff
parent 75126 da1108a6d249
child 75128 8c7bdd68a47a
more robust startup wrt. VSCode workspace (by Fabian Huch);
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue Feb 22 11:53:06 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Feb 22 12:23:21 2022 +0100
@@ -30,10 +30,10 @@
     window.showErrorMessage("Missing user settings: isabelle.home")
   else {
     const workspace_dir = await Isabelle_FSP.register(context)
-    const roots = await workspace.findFiles("{ROOT,ROOTS}")
+    const roots = workspace.workspaceFile === undefined ? await workspace.findFiles("{ROOT,ROOTS}") : []
     const isabelle_tool = isabelle_home + "/bin/isabelle"
     const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
-    const session_args = roots.length > 0 ? ["-D", workspace_dir] : []
+    const session_args = roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : []
 
     const server_options: ServerOptions =
       library.platform_is_windows() ?
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts	Tue Feb 22 11:53:06 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts	Tue Feb 22 12:23:21 2022 +0100
@@ -74,6 +74,7 @@
   private static instance: Isabelle_FSP
   private static state: Workspace_State
   private static readonly draft_session = 'Draft'
+  private static readonly session_dir = 'Isabelle Sessions'
 
   //#region public static API
 
@@ -82,7 +83,7 @@
   public static readonly theory_extension = '.thy'
   public static readonly theory_files_glob = '**/*.thy'
 
-  public static register(context: ExtensionContext): Promise<string>
+  public static register(context: ExtensionContext): Promise<string|undefined>
   {
     this.instance = new Isabelle_FSP()
     this.state = new Workspace_State(context)
@@ -215,26 +216,26 @@
 
   //#region initialization
 
-  private async setup_workspace(): Promise<string>
+  private async setup_workspace(): Promise<string|undefined>
   {
     const { state } = Isabelle_FSP
     let { sessions, workspace_dir, symbol_entries } = state.get_setup_data()
-    const main_folder_uri = Isabelle_FSP.get_dir_uri('')
 
-    if (workspace.workspaceFolders[0].uri.toString() !== main_folder_uri.toString()) {
+    const workspace_folders = workspace.workspaceFolders || []
+    const isabelle_folder = workspace_folders.find(folder =>
+       folder.name === Isabelle_FSP.session_dir && folder.uri.scheme === Isabelle_FSP.scheme)
+
+    if (isabelle_folder === undefined) {
       workspace.updateWorkspaceFolders(0, 0,
-        {
-          uri: main_folder_uri,
-          name: 'Isabelle Sessions'
-        }
-      )
+        { uri: Isabelle_FSP.get_dir_uri(''), name: Isabelle_FSP.session_dir })
     }
 
     if (sessions && workspace_dir && symbol_entries) {
       await Isabelle_FSP.update_symbol_encoder(symbol_entries)
       await this.init_filesystem(sessions)
     } else {
-      workspace_dir = workspace.workspaceFolders[1].uri.fsPath
+      const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_FSP.scheme)
+      if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath
     }
 
     await state.set(State_Key.workspace_dir, workspace_dir)
@@ -423,6 +424,7 @@
 
   private async load_theory(file_uri: Uri, isabelle_uri: Uri)
   {
+    if (!this.symbol_encoder) return
     const data = await workspace.fs.readFile(file_uri)
     const encoded_data = this.symbol_encoder.encode(data)
     await this.writeFile(isabelle_uri, encoded_data, { create: true, overwrite: true })
@@ -453,6 +455,7 @@
 
   private async open_theory_dialogue(file_uri: Uri)
   {
+    if (!this.symbol_encoder) return
     const always_open = library.get_configuration<boolean>('always_open_thys')
     if (!always_open) {
       const answer = await window.showInformationMessage(
@@ -473,6 +476,7 @@
 
   private async reload_theory(file_uri: Uri, isabelle_uri: Uri)
   {
+    if (!this.symbol_encoder) return
     const data = await workspace.fs.readFile(file_uri)
     const encoded_data = this.symbol_encoder.encode(data)
     await this.writeFile(isabelle_uri, encoded_data, { create: false, overwrite: true })
@@ -562,6 +566,7 @@
 
   private async sync_original(uri: Uri, content: Uint8Array)
   {
+    if (!this.symbol_encoder) return
     const origin_uri = this.file_to_isabelle.get_from(uri)
     const decoded_content = this.symbol_encoder.decode(content)
     workspace.fs.writeFile(origin_uri, decoded_content)