# HG changeset patch # User wenzelm # Date 1646334267 -3600 # Node ID 4187f6f18232b075d2c9b1f75de17faf25caaf92 # Parent 31c5a22d50ef8d6fcc3ec2018d5d03d9474bccd3 provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol; diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/etc/settings --- 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" diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/extension.ts --- 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) }) diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts --- 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 + public static register(context: ExtensionContext, symbols: symbol.Symbols): Promise { 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 { 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 } diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts --- 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 - { - 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) diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts --- 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(State_Key.sessions), - symbol_entries: this.get(State_Key.symbol_entries) + sessions: this.get(State_Key.sessions) } } diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/library.ts --- 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 +} diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/lsp.ts --- 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("PIDE/preview_response") -/* Isabelle symbols */ - -export interface Symbols -{ - entries: [symbol.Entry] -} - -export const symbols_type = - new NotificationType("PIDE/symbols") - -export const symbols_request_type = - new NotificationType("PIDE/symbols_request") +/* session theories */ export interface Entries { @@ -142,6 +131,7 @@ export const session_theories_request_type = new NotificationType("PIDE/session_theories_request") + /* spell checker */ export const include_word_type = diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/extension/src/symbol.ts --- 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() -const codes = new Map() - -export function get_name(sym: Symbol): string | undefined +export class Symbols { - return names.get(sym) -} + entries: [Entry] + private entries_map: Map + + constructor(entries: [Entry]) + { + this.entries = entries + this.entries_map = new Map() + 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 { - 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) } diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/src/language_server.scala --- 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") diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/src/lsp.scala --- 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") diff -r 31c5a22d50ef -r 4187f6f18232 src/Tools/VSCode/src/vscode_setup.scala --- 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)")