provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol;

--- a/src/Tools/VSCode/etc/settings	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/etc/settings	Thu Mar 03 20:04:27 2022 +0100
@@ -3,3 +3,4 @@
 ISABELLE_VSCODE_VERSION="1.64.2"
 ISABELLE_VSCODE_HOME="$ISABELLE_HOME/src/Tools/VSCode"
 ISABELLE_VSCODE_SETTINGS="$ISABELLE_HOME_USER/vscode"
+ISABELLE_VSCODE_WORKSPACE="$ISABELLE_VSCODE_SETTINGS/workspace"

--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -3,6 +3,7 @@
 import * as platform from './platform'
 import * as library from './library'
 import * as file from './file'
+import * as symbol from './symbol'
 import * as vscode_lib from './vscode_lib'
 import * as decorations from './decorations'
 import * as preview_panel from './preview_panel'
@@ -25,7 +26,8 @@
   try {
     const isabelle_home = library.getenv_strict("ISABELLE_HOME")
 
-    const workspace_dir = await Isabelle_Workspace.register(context)
+    const symbols = await symbol.load_symbols(library.workspace_path("symbols.json"))
+    const workspace_dir = await Isabelle_Workspace.register(context, symbols)
     const roots = workspace.workspaceFile === undefined ? await workspace.findFiles("{ROOT,ROOTS}") : []
 
     const isabelle_tool = isabelle_home + "/bin/isabelle"
@@ -173,19 +175,7 @@
       language_client.onNotification(lsp.session_theories_type,
         async ({entries}) => await Isabelle_Workspace.update_sessions(entries))
 
-      language_client.onNotification(lsp.symbols_type,
-        params =>
-          {
-            //register_abbreviations(params.entries, context)
-            Isabelle_Workspace.update_symbol_encoder(params.entries)
-
-            // request theories to load in isabelle file system
-            // after a valid symbol encoder is loaded
-            language_client.sendNotification(lsp.session_theories_request_type)
-          })
-
-      language_client.sendNotification(lsp.symbols_request_type)
-
+      language_client.sendNotification(lsp.session_theories_request_type)
     })
 
 

--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -35,11 +35,11 @@
   public static readonly theory_extension = '.thy'
   public static readonly theory_files_glob = '**/*.thy'
 
-  public static register(context: ExtensionContext): Promise<string|undefined>
+  public static register(context: ExtensionContext, symbols: symbol.Symbols): Promise<string|undefined>
   {
     this.state = new Workspace_State(context)
     
-    const encoder = new Symbol_Encoder(this.state.get(State_Key.symbol_entries) || [])
+    const encoder = new Symbol_Encoder(symbols.entries)
     this.instance = new Isabelle_Workspace()
     this.instance.fs = new Mapping_FSP(Isabelle_Workspace.theory_files_glob, Isabelle_Workspace.scheme, encoder)
 
@@ -71,12 +71,6 @@
     return Uri.parse(`${Isabelle_Workspace.scheme}:/${session}/${rel_path}`)
   }
 
-  public static async update_symbol_encoder(entries: symbol.Entry[])
-  {
-    this.instance.fs.update_symbol_encoder(new Symbol_Encoder(entries))
-    await this.state.set(State_Key.symbol_entries, entries)
-  }
-
   public static async update_sessions(sessions: Session_Theories[])
   {
     await Isabelle_Workspace.state.set(State_Key.sessions, sessions)
@@ -142,7 +136,7 @@
   private async setup_workspace(): Promise<string|undefined>
   {
     const { state } = Isabelle_Workspace
-    let { sessions, workspace_dir, symbol_entries } = state.get_setup_data()
+    let { sessions, workspace_dir } = state.get_setup_data()
 
     const workspace_folders = workspace.workspaceFolders || []
     const isabelle_folder = workspace_folders.find(folder =>
@@ -153,10 +147,10 @@
         { 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)
+    if (sessions && workspace_dir) {
       await this.load_tree_state(sessions)
-    } else {
+    }
+    else {
       const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_Workspace.scheme)
       if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath
     }

--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -83,13 +83,6 @@
   }
 
 
-  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
   {
     const watcher = workspace.createFileSystemWatcher(this.glob)

--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -13,14 +13,12 @@
 {
   workspace_dir: string
   sessions: Session_Theories[]
-  symbol_entries: symbol.Entry[]
 }
 
 enum State_Key
 {
   workspace_dir = 'workspace_dir',
-  sessions = 'sessions',
-  symbol_entries = 'symbol_entries'
+  sessions = 'sessions'
 }
 
 class Workspace_State
@@ -31,8 +29,7 @@
   {
     return {
       workspace_dir: this.get(State_Key.workspace_dir),
-      sessions: this.get<Session_Theories[]>(State_Key.sessions),
-      symbol_entries: this.get<symbol.Entry[]>(State_Key.symbol_entries)
+      sessions: this.get<Session_Theories[]>(State_Key.sessions)
     }
   }
 

--- a/src/Tools/VSCode/extension/src/library.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -48,3 +48,8 @@
   if (s) return s
   else throw new Error("Undefined Isabelle environment variable: " + quote(name))
 }
+
+export function workspace_path(path: string): string
+{
+  return getenv_strict("ISABELLE_VSCODE_WORKSPACE") + "/" + path
+}

--- a/src/Tools/VSCode/extension/src/lsp.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -112,18 +112,7 @@
   new NotificationType<Preview_Response>("PIDE/preview_response")
 
 
-/* Isabelle symbols */
-
-export interface Symbols
-{
-  entries: [symbol.Entry]
-}
-
-export const symbols_type =
-  new NotificationType<Symbols>("PIDE/symbols")
-
-export const symbols_request_type =
-  new NotificationType<void>("PIDE/symbols_request")
+/* session theories */
 
 export interface Entries<T>
 {
@@ -142,6 +131,7 @@
 export const session_theories_request_type =
   new NotificationType<void>("PIDE/session_theories_request")
 
+
 /* spell checker */
 
 export const include_word_type =

--- a/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 20:04:27 2022 +0100
@@ -6,7 +6,7 @@
 'use strict';
 
 import * as library from './library'
-import { Disposable, DocumentSelector, ExtensionContext, extensions, window } from 'vscode'
+import * as file from './file'
 
 
 /* ASCII characters */
@@ -39,7 +39,7 @@
 }
 
 
-/* named symbols */
+/* defined symbols */
 
 export interface Entry
 {
@@ -49,33 +49,40 @@
   abbrevs: string[]
 }
 
-let symbol_entries: [Entry]
-const names = new Map<Symbol, string>()
-const codes = new Map<Symbol, number>()
-
-export function get_name(sym: Symbol): string | undefined
+export class Symbols
 {
-  return names.get(sym)
-}
+  entries: [Entry]
+  private entries_map: Map<Symbol, Entry>
+
+  constructor(entries: [Entry])
+  {
+    this.entries = entries
+    this.entries_map = new Map<Symbol, Entry>()
+    for (const entry of entries) {
+      this.entries_map.set(entry.symbol, entry)
+    }
+  }
 
-export function get_code(sym: Symbol): number | undefined
-{
-  return codes.get(sym)
+  public get(sym: Symbol): Entry | undefined
+  {
+    return this.entries_map.get(sym)
+  }
+
+  public defined(sym: Symbol): boolean
+  {
+    return this.entries_map.has(sym)
+  }
+
+  public decode(sym: Symbol): string | undefined
+  {
+    const entry = this.get(sym)
+    const code = entry ? entry.code : undefined
+    return code ? String.fromCharCode(code) : undefined
+  }
 }
 
-export function get_unicode(sym: Symbol): string
-{
-  const code = get_code(sym)
-  return code ? String.fromCharCode(code) : ""
-}
-
-function update_entries(entries: [Entry])
+export async function load_symbols(path: string): Promise<Symbols>
 {
-  symbol_entries = entries
-  names.clear
-  codes.clear
-  for (const entry of entries) {
-    names.set(entry.symbol, entry.name)
-    codes.set(entry.symbol, entry.code)
-  }
+  const entries = await file.read_json<[Entry]>(file.platform_path(path))
+  return new Symbols(entries)
 }

--- a/src/Tools/VSCode/src/language_server.scala	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Thu Mar 03 20:04:27 2022 +0100
@@ -485,7 +485,6 @@
           case LSP.State_Update(id) => State_Panel.update(id)
           case LSP.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
           case LSP.Preview_Request(file, column) => request_preview(file, column)
-          case LSP.Symbols_Request(()) => channel.write(LSP.Symbols())
           case LSP.Session_Theories_Request(()) =>
             channel.write(LSP.Session_Theories(session_theories))
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")

--- a/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Thu Mar 03 20:04:27 2022 +0100
@@ -624,26 +624,6 @@
   }
 
 
-  /* Isabelle symbols */
-
-  object Symbols_Request extends Notification0("PIDE/symbols_request")
-
-  object Symbols
-  {
-    def apply(): JSON.T =
-    {
-      val entries =
-        for (entry <- Symbol.symbols.entries; code <- entry.code)
-        yield JSON.Object(
-          "symbol" -> entry.symbol,
-          "name" -> entry.name,
-          "code" -> code,
-          "abbrevs" -> entry.abbrevs
-        )
-      Notification("PIDE/symbols", JSON.Object("entries" -> entries))
-    }
-  }
-
   /* Session structure */
 
   object Session_Theories_Request extends Notification0("PIDE/session_theories_request")

--- a/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 03 19:51:00 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Thu Mar 03 20:04:27 2022 +0100
@@ -21,6 +21,7 @@
   def vscode_settings: Path = Path.variable("ISABELLE_VSCODE_SETTINGS")
   def vscode_settings_user: Path = vscode_settings + Path.explode("user-data/User/settings.json")
   def vscode_version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION")
+  def vscode_workspace: Path = Path.variable("ISABELLE_VSCODE_WORKSPACE")
 
   def exe_path(dir: Path): Path = dir + Path.explode("bin/codium")
 
@@ -69,6 +70,27 @@
   }
 
 
+  /* workspace */
+
+  def init_workspace(dir: Path): Unit =
+  {
+    Isabelle_System.make_directory(dir)
+    Isabelle_System.chmod("700", dir)
+
+    File.change(dir + Path.explode("symbols.json"), init = true) { _ =>
+      JSON.Format(
+        for (entry <- Symbol.symbols.entries; code <- entry.code)
+          yield JSON.Object(
+            "symbol" -> entry.symbol,
+            "name" -> entry.name,
+            "code" -> code,
+            "abbrevs" -> entry.abbrevs
+          )
+      )
+    }
+  }
+
+
   /* vscode setup */
 
   val default_download_url: String = "https://github.com/VSCodium/vscodium/releases/download"
@@ -117,7 +139,10 @@
     }
 
     if (check) {
-      if (install_ok) progress.echo(install_dir.expand.implode)
+      if (install_ok) {
+        init_workspace(vscode_workspace)
+        progress.echo(install_dir.expand.implode)
+      }
       else {
         error("Bad Isabelle/VSCode installation: " + install_dir.expand +
           "\n(use \"isabelle vscode_setup\" for download and installation)")