# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1645654659 -3600
# Node ID 4c3115f94b6e7d788a450ddc34ed12b83c1d274f
# Parent  8dd7f013026665b612efd1eb2724a1cce45d58d5
tuned vscode extension;

diff -r 8dd7f0130266 -r 4c3115f94b6e src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Wed Feb 23 22:12:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Wed Feb 23 23:17:39 2022 +0100
@@ -170,7 +170,7 @@
     language_client.onReady().then(() =>
     {
       language_client.onNotification(protocol.session_theories_type,
-        async ({entries}) => await Isabelle_Workspace.init_workspace(entries))
+        async ({entries}) => await Isabelle_Workspace.update_sessions(entries))
 
       language_client.onNotification(protocol.symbols_type,
         params =>
diff -r 8dd7f0130266 -r 4c3115f94b6e src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Wed Feb 23 22:12:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Wed Feb 23 23:17:39 2022 +0100
@@ -73,9 +73,10 @@
     await this.state.set(State_Key.symbol_entries, entries)
   }
 
-  public static async init_workspace(sessions: Session_Theories[])
+  public static async update_sessions(sessions: Session_Theories[])
   {
-    await this.instance.init_filesystem(sessions)
+    await Isabelle_Workspace.state.set(State_Key.sessions, sessions)
+    await this.instance.load_tree_state(sessions)
     for (const doc of workspace.textDocuments) {
       await this.instance.open_workspace_document(doc)
     }
@@ -86,12 +87,12 @@
 
   public static get_isabelle(file_uri: Uri): Uri
   {
-    return this.instance.fs.file_to_entry.get_to(file_uri) || file_uri
+    return this.instance.fs.get_entry(file_uri) || file_uri
   }
 
   public static get_file(isabelle_uri: Uri): Uri
   {
-    return this.instance.fs.file_to_entry.get_from(isabelle_uri) || isabelle_uri
+    return this.instance.fs.get_file(isabelle_uri) || isabelle_uri
   }
 
   public async open_workspace_document(doc: TextDocument)
@@ -102,11 +103,11 @@
       }
     } else {
       if (doc.languageId === Isabelle_Workspace.isabelle_lang_id) {
-        const isabelle_uri = this.fs.file_to_entry.get_to(doc.uri)
+        const isabelle_uri = this.fs.get_entry(doc.uri)
         if (!isabelle_uri) {
           await this.create_mapping_load_theory(doc.uri)
         } else if (!this.is_open_theory(isabelle_uri)) {
-          await this.fs.load(doc.uri, isabelle_uri)
+          await this.fs.reload(doc.uri, isabelle_uri)
         }
       }
     }
@@ -119,7 +120,7 @@
         Isabelle_Workspace.warn_not_synchronized(doc.fileName)
       }
     } else if (doc.fileName.endsWith(Isabelle_Workspace.theory_extension)) {
-      const isabelle_uri = this.fs.file_to_entry.get_to(doc.uri)
+      const isabelle_uri = this.fs.get_entry(doc.uri)
       if (!isabelle_uri || !this.is_open_theory(isabelle_uri)) {
         await this.open_theory_dialogue(doc.uri)
       }
@@ -129,7 +130,7 @@
   public async reload(doc: Uri)
   {
     if (doc.scheme === Isabelle_Workspace.scheme) {
-      const file_uri = this.fs.file_to_entry.get_from(doc)
+      const file_uri = this.fs.get_file(doc)
       await this.fs.reload(file_uri, doc)
     }
   }
@@ -145,40 +146,28 @@
 
     if (isabelle_folder === undefined) {
       workspace.updateWorkspaceFolders(0, 0,
-        { uri: Isabelle_Workspace.instance.fs.get_dir_uri(''), name: Isabelle_Workspace.session_dir })
+        { uri: Isabelle_Workspace.instance.get_dir_uri(''), name: Isabelle_Workspace.session_dir })
     }
 
     if (sessions && workspace_dir && symbol_entries) {
       await Isabelle_Workspace.update_symbol_encoder(symbol_entries)
-      await this.init_filesystem(sessions)
+      await this.load_tree_state(sessions)
     } else {
       const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_Workspace.scheme)
       if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath
     }
 
     await state.set(State_Key.workspace_dir, workspace_dir)
-    await this.save_tree_state()
-    this.fs.onDidChangeFile(events => {
-      for (const e of events) {
-        if (e.type === FileChangeType.Changed) continue
-
-        this.save_tree_state()
-        return
-      }
-    })
     return workspace_dir
   }
 
-  private async init_filesystem(sessions: Session_Theories[])
+  private async load_tree_state(sessions: Session_Theories[])
   {
-    const all_theory_uris = sessions
-      .map(s => s.theories)
-      .reduce((acc,x) => acc.concat(x), [])
+    const root_entries = this.fs.list_dirs(this.get_dir_uri(''))
+    for (const key of root_entries) {
+      this.fs.remove(this.get_dir_uri(key))
+    }
 
-    // clean old files
-    this.fs.clear(all_theory_uris)
-
-    // create new
     for (const { session_name, theories: theories_uri } of sessions) {
       if (!session_name) continue
       if (session_name !== Isabelle_Workspace.draft_session) {
@@ -188,7 +177,7 @@
         })
       }
 
-      this.fs.make_dir(session_name)
+      this.fs.make_dir(this.get_dir_uri(session_name))
 
       for (const theory_uri of theories_uri) {
         await this.create_mapping_load_theory(Uri.parse(theory_uri))
@@ -206,15 +195,13 @@
   {
     const session = this.get_session(file_uri)
     const isabelle_uri = this.create_new_uri(file_uri, session)
-    this.fs.file_to_entry.add(file_uri, isabelle_uri)
-
     await this.fs.load(file_uri, isabelle_uri)
     return isabelle_uri
   }
 
   private async is_workspace_theory(isabelle_uri: Uri): Promise<boolean>
   {
-    const file_uri = this.fs.file_to_entry.get_from(isabelle_uri)
+    const file_uri = this.fs.get_file(isabelle_uri)
     const files = await workspace.findFiles(Isabelle_Workspace.theory_files_glob)
     return !!(files.find(uri => uri.toString() === file_uri.toString()))
   }
@@ -250,7 +237,7 @@
   {
     let session = this.session_theories.find((s) => s.theories.includes(file_uri.toString()))
     if (!session) {
-      this.fs.make_dir(Isabelle_Workspace.draft_session)
+      this.fs.make_dir(this.get_dir_uri(Isabelle_Workspace.draft_session))
       return Isabelle_Workspace.draft_session
     }
 
@@ -265,9 +252,9 @@
     let fs_path = file_uri.fsPath
     while (true) {
       const discriminator = extra ? ` (${extra})` : ''
-      new_uri = this.fs.get_uri(session_name, file_name + discriminator)
+      new_uri = this.get_uri(session_name, file_name + discriminator)
 
-      const old_uri = this.fs.file_to_entry.get_from(new_uri)
+      const old_uri = this.fs.get_file(new_uri)
       if (!old_uri || old_uri.toString() === file_uri.toString()) {
         return new_uri
       }
@@ -280,9 +267,4 @@
       extra = path.posix.join(path.posix.basename(fs_path), extra)
     }
   }
-
-  private async save_tree_state()
-  {
-    await Isabelle_Workspace.state.set(State_Key.sessions, this.fs.get_tree_state())
-  }
-}
+}
\ No newline at end of file
diff -r 8dd7f0130266 -r 4c3115f94b6e src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts	Wed Feb 23 22:12:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts	Wed Feb 23 23:17:39 2022 +0100
@@ -65,17 +65,20 @@
 export class Mapping_FSP implements FileSystemProvider
 {
   private root = new Directory('')
-  file_to_entry = new Uri_Map()
+  private file_to_entry = new Uri_Map()
   private symbol_encoder: Symbol_Encoder
   private readonly scheme: string
   private readonly glob: GlobPattern
 
+  
   constructor(glob: GlobPattern, scheme: string, encoder: Symbol_Encoder) 
   {
+    this.glob = glob
     this.scheme = scheme
     this.symbol_encoder = encoder
   }
 
+
   public update_symbol_encoder(encoder: Symbol_Encoder)
   {
     this.symbol_encoder = encoder
@@ -88,61 +91,119 @@
       const entry = this.file_to_entry.get_to(file)
       if (entry) this.reload(file, entry)
     })
-    watcher.onDidDelete(file => this._delete(this.file_to_entry.get_to(file)))
+    watcher.onDidDelete(file => this.remove(this.file_to_entry.get_to(file), true))
     return watcher
   }
 
-  private async sync_original(uri: Uri, content: Uint8Array)
+
+  public get_entry(file: Uri): Uri | undefined
+  {
+    return this.file_to_entry.get_to(file)
+  }
+
+  public get_file(entry: Uri): Uri | undefined
   {
-    const origin_uri = this.file_to_entry.get_from(uri)
-    const decoded_content = this.symbol_encoder.decode(content)
-    workspace.fs.writeFile(origin_uri, decoded_content)
+    return this.file_to_entry.get_from(entry)
+  }
+
+
+  private get_parent_data(uri: Uri): [Directory, Uri]
+  {
+    const parent_uri = uri.with({ path: path.posix.dirname(uri.path) })
+    const parent = this.lookup_directory(parent_uri, false)
+
+    return [parent, parent_uri]
   }
 
-  public get_dir_uri(session: string): Uri
-  {
-    return Uri.parse(`${this.scheme}:/${session}`)
+  private lookup(uri: Uri, silent: false): Entry
+  private lookup(uri: Uri, silent: boolean): Entry | undefined
+  private lookup(uri: Uri, silent: boolean): Entry | undefined {
+    const parts = uri.path.split('/')
+    let entry: Entry = this.root
+    for (const part of parts) {
+      if (!part) {
+        continue
+      }
+      let child: Entry | undefined
+      if (entry instanceof Directory) {
+        child = entry.entries.get(part)
+      }
+      if (!child) {
+        if (!silent) {
+          throw FileSystemError.FileNotFound(uri)
+        } else {
+          return undefined
+        }
+      }
+      entry = child
+    }
+    return entry
   }
 
-  public get_uri(session: string, rel_path: String): Uri
+  private lookup_directory(uri: Uri, silent: boolean): Directory
   {
-    return Uri.parse(`${this.scheme}:/${session}/${rel_path}`)
+    const entry = this.lookup(uri, silent)
+    if (entry instanceof Directory) {
+      return entry
+    }
+    throw FileSystemError.FileNotADirectory(uri)
+  }
+
+  private lookup_file(uri: Uri, silent: boolean): File
+  {
+    const entry = this.lookup(uri, silent)
+    if (entry instanceof File) {
+      return entry
+    }
+    throw FileSystemError.FileIsADirectory(uri)
   }
-  
+
+  public list_dirs(uri: Uri): string[]
+  {
+    const res: string[] = []
+    for (const [name, dir] of this.lookup_directory(uri, false).entries) {
+      if (dir instanceof Directory) {
+        res.push(dir.name)
+      }
+    }
+    
+    return res
+  }
 
-  // #region create
-  
-  private _create_directory(uri: Uri): void
+  public list_files(uri: Uri): string[]
+  {
+    const res: string[] = []
+    for (const [name, dir] of this.lookup_directory(uri, false).entries) {
+      if (dir instanceof File) {
+        res.push(dir.name)
+      }
+    }
+    
+    return res
+  }
+
+
+  public make_dir(uri: Uri): void
   {
     const basename = path.posix.basename(uri.path)
-    const [parent, parent_uri] = this._get_parent_data(uri)
+    const [parent, parent_uri] = this.get_parent_data(uri)
 
-    const entry = new Directory(basename)
-    parent.entries.set(entry.name, entry)
-    parent.mtime = Date.now()
-    parent.size += 1
-    this._fire_soon(
-      { type: FileChangeType.Changed, uri: parent_uri },
-      { type: FileChangeType.Created, uri }
-    )
-  }
-
-  public make_dir(name: string)
-  {
-    const root_entries = Array.from(this.root.entries.keys())
-
-    if (!root_entries.includes(name)) {
-      this._create_directory(this.get_dir_uri(name))
+    if (!parent.entries.has(basename)) {
+      const entry = new Directory(basename)
+      parent.entries.set(entry.name, entry)
+      parent.mtime = Date.now()
+      parent.size += 1
+      this.fire_soon(
+        { type: FileChangeType.Changed, uri: parent_uri },
+        { type: FileChangeType.Created, uri }
+      )
     }
   }
 
-  // #endregion
-
-
-  // #region read
 
   public async load(file_uri: Uri, isabelle_uri: Uri)
   {
+    this.file_to_entry.add(file_uri, isabelle_uri)
     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 })
@@ -155,16 +216,19 @@
     await this.writeFile(isabelle_uri, encoded_data, { create: false, overwrite: true })
   }
 
-  // #endregion
+  private async sync_original(uri: Uri, content: Uint8Array)
+  {
+    const origin_uri = this.file_to_entry.get_from(uri)
+    const decoded_content = this.symbol_encoder.decode(content)
+    workspace.fs.writeFile(origin_uri, decoded_content)
+  }
 
 
-  // #region delete
-
-  _delete(uri: Uri, silent: boolean = false): void
+  remove(uri: Uri, silent: boolean = false): void
   {
     const dirname = uri.with({ path: path.posix.dirname(uri.path) })
     const basename = path.posix.basename(uri.path)
-    const parent = this._lookup_directory(dirname, silent)
+    const parent = this.lookup_directory(dirname, silent)
 
     if (!parent) return
     if (!parent.entries.has(basename)) {
@@ -179,12 +243,12 @@
     parent.mtime = Date.now()
     parent.size -= 1
 
-    this._fire_soon({ type: FileChangeType.Changed, uri: dirname }, { uri, type: FileChangeType.Deleted })
+    this.fire_soon({ type: FileChangeType.Changed, uri: dirname }, { uri, type: FileChangeType.Deleted })
   }
 
   private sync_deletion(isabelle_uri: Uri, silent: boolean)
   {
-    const dir = this._lookup(isabelle_uri, silent)
+    const dir = this.lookup(isabelle_uri, silent)
     if (!dir) {
       if (silent)
         return
@@ -209,128 +273,30 @@
     }
   }
 
-  public clear(all_theory_uris: string[])
-  {
-    const root_entries = Array.from(this.root.entries.keys())
 
-    for (const key of root_entries) {
-      if (key === 'Draft') {
-        const draft = this.root.entries.get(key)
-
-        if (draft instanceof Directory) {
-          for (const draft_thy of draft.entries.keys()) {
-            const isabelle_uri = this.get_uri('Draft', draft_thy)
-            const file_uri = this.file_to_entry.get_from(isabelle_uri)
-
-            if (file_uri && all_theory_uris.includes(file_uri.toString())) {
-              this._delete(isabelle_uri)
-            }
-          }
-        }
-      } else {
-        this._delete(this.get_dir_uri(key), true)
-      }
-    }
-  }
-
-  // #endregion
-
-  private _get_parent_data(uri: Uri): [Directory, Uri]
-  {
-    const parent_uri = uri.with({ path: path.posix.dirname(uri.path) })
-    const parent = this._lookup_directory(parent_uri, false)
-
-    return [parent, parent_uri]
-  }
+  private buffered_events: FileChangeEvent[] = []
+  private fire_soon_handle?: NodeJS.Timer
 
-  private _lookup(uri: Uri, silent: false): Entry
-  private _lookup(uri: Uri, silent: boolean): Entry | undefined
-  private _lookup(uri: Uri, silent: boolean): Entry | undefined {
-    const parts = uri.path.split('/')
-    let entry: Entry = this.root
-    for (const part of parts) {
-      if (!part) {
-        continue
-      }
-      let child: Entry | undefined
-      if (entry instanceof Directory) {
-        child = entry.entries.get(part)
-      }
-      if (!child) {
-        if (!silent) {
-          throw FileSystemError.FileNotFound(uri)
-        } else {
-          return undefined
-        }
-      }
-      entry = child
-    }
-    return entry
-  }
-
-  private _lookup_directory(uri: Uri, silent: boolean): Directory
-  {
-    const entry = this._lookup(uri, silent)
-    if (entry instanceof Directory) {
-      return entry
-    }
-    throw FileSystemError.FileNotADirectory(uri)
-  }
-
-  private _lookup_file(uri: Uri, silent: boolean): File
+  private fire_soon(...events: FileChangeEvent[]): void
   {
-    const entry = this._lookup(uri, silent)
-    if (entry instanceof File) {
-      return entry
-    }
-    throw FileSystemError.FileIsADirectory(uri)
-  }
-
-  public get_tree_state(): Session_Theories[]
-  {
-    const sessions: Session_Theories[] = []
-    for (const [session_name, val] of this.root.entries) {
-      if (!(val instanceof Directory)) return
-      const theories: string[] = []
+    this.buffered_events.push(...events)
 
-      for (const fileName of val.entries.keys()) {
-        const file = this.file_to_entry.get_from(this.get_uri(session_name, fileName))
-        theories.push(file.toString())
-      }
-
-      sessions.push({session_name, theories})
-    }
-    return sessions
-  }
-
-
-  //#region events
-
-  private _buffered_events: FileChangeEvent[] = []
-  private _fire_soon_handle?: NodeJS.Timer
-
-  private _fire_soon(...events: FileChangeEvent[]): void
-  {
-    this._buffered_events.push(...events)
-
-    if (this._fire_soon_handle) {
-      clearTimeout(this._fire_soon_handle)
+    if (this.fire_soon_handle) {
+      clearTimeout(this.fire_soon_handle)
     }
 
-    this._fire_soon_handle = setTimeout(() => {
-      this._emitter.fire(this._buffered_events)
-      this._buffered_events.length = 0
+    this.fire_soon_handle = setTimeout(() => {
+      this.emitter.fire(this.buffered_events)
+      this.buffered_events.length = 0
     }, 5)
   }
 
-  private _emitter = new EventEmitter<FileChangeEvent[]>()
-
-  //#endregion
+  private emitter = new EventEmitter<FileChangeEvent[]>()
 
 
   //#region fsp implementation
 
-  readonly onDidChangeFile: Event<FileChangeEvent[]> = this._emitter.event
+  readonly onDidChangeFile: Event<FileChangeEvent[]> = this.emitter.event
 
   watch(_resource: Uri): Disposable
   {
@@ -339,12 +305,12 @@
 
   stat(uri: Uri): FileStat
   {
-    return this._lookup(uri, false)
+    return this.lookup(uri, false)
   }
 
   readDirectory(uri: Uri): [string, FileType][]
   {
-    const entry = this._lookup_directory(uri, false)
+    const entry = this.lookup_directory(uri, false)
     const result: [string, FileType][] = []
     for (const [name, child] of entry.entries) {
       result.push([name, child.type])
@@ -359,7 +325,7 @@
 
   readFile(uri: Uri): Uint8Array
   {
-    const data = this._lookup_file(uri, false).data
+    const data = this.lookup_file(uri, false).data
     if (data) {
       return data
     }
@@ -373,7 +339,7 @@
     }
 
     const basename = path.posix.basename(isabelle_uri.path)
-    const [parent, parent_uri] = this._get_parent_data(isabelle_uri)
+    const [parent, parent_uri] = this.get_parent_data(isabelle_uri)
     let entry = parent.entries.get(basename)
     if (entry instanceof Directory) {
       throw FileSystemError.FileIsADirectory(isabelle_uri)
@@ -394,7 +360,7 @@
       entry.size = content.byteLength
       entry.data = content
 
-      this._fire_soon({ type: FileChangeType.Changed, uri: isabelle_uri })
+      this.fire_soon({ type: FileChangeType.Changed, uri: isabelle_uri })
       return
     }
 
@@ -406,7 +372,7 @@
     parent.entries.set(basename, entry)
     parent.mtime = Date.now()
     parent.size++
-    this._fire_soon(
+    this.fire_soon(
       { type: FileChangeType.Changed, uri: parent_uri },
       { type: FileChangeType.Created, uri: isabelle_uri }
     )
@@ -414,14 +380,14 @@
 
   delete(uri: Uri): void
   {
-    const [parent, parent_uri] = this._get_parent_data(uri)
+    const [parent, parent_uri] = this.get_parent_data(uri)
     if (parent && parent.name === 'Draft') {
       if (parent.size === 1) {
-        this._delete(parent_uri)
+        this.remove(parent_uri)
         return
       }
 
-      this._delete(uri)
+      this.remove(uri)
       return
     }