updated vscode extension: proper recoding;
authorFabian Huch <huch@in.tum.de>
Wed, 23 Feb 2022 23:24:26 +0100
changeset 75137 6b29b37de52e
parent 75136 4c3115f94b6e
child 75138 cd77ffb01e15
updated vscode extension: proper recoding;
src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts
src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts	Wed Feb 23 23:17:39 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts	Wed Feb 23 23:24:26 2022 +0100
@@ -79,9 +79,11 @@
   }
 
 
-  public update_symbol_encoder(encoder: Symbol_Encoder)
+  public async update_symbol_encoder(encoder: Symbol_Encoder): Promise<void>
   {
     this.symbol_encoder = encoder
+    await Promise.all(this.file_to_entry.keys().map(file =>
+       this.reload(file, this.file_to_entry.get_to(file))))
   }
 
   public sync_subscription(): Disposable
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts	Wed Feb 23 23:17:39 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts	Wed Feb 23 23:24:26 2022 +0100
@@ -12,6 +12,11 @@
     return Uri.parse(uri.toString())
   }
 
+  public keys(): Uri[]
+  {
+    return [...this.rev_map.values()]
+  }
+
   public add(from: Uri, to: Uri)
   {
     const norm_from = Uri_Map.normalize(from)