# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1645655066 -3600
# Node ID 6b29b37de52e2b8a81d54070420b4d9a2842c360
# Parent  4c3115f94b6e7d788a450ddc34ed12b83c1d274f
updated vscode extension: proper recoding;

diff -r 4c3115f94b6e -r 6b29b37de52e src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.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
diff -r 4c3115f94b6e -r 6b29b37de52e src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts
--- 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)