--- 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)