# HG changeset patch # User Fabian Huch # Date 1645650720 -3600 # Node ID 8dd7f013026665b612efd1eb2724a1cce45d58d5 # Parent c04ccea8bdd2fcd2e2554f45753edf5490fd0f2e tuned vscode extension: split isabelle fsp into workspace and mapping; diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Wed Feb 23 10:46:10 2022 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Wed Feb 23 22:12:00 2022 +0100 @@ -6,7 +6,7 @@ TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode' import { Document_Decorations } from './protocol' import * as library from './library' -import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp' +import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace' /* known decoration types */ @@ -169,7 +169,7 @@ export function apply_decoration(decorations: Document_Decorations) { - const uri = Isabelle_FSP.get_isabelle(Uri.parse(decorations.uri)) + const uri = Isabelle_Workspace.get_isabelle(Uri.parse(decorations.uri)) for (const decoration of decorations.entries) { const typ = types.get(decoration.type) diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Wed Feb 23 10:46:10 2022 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Wed Feb 23 22:12:00 2022 +0100 @@ -10,7 +10,7 @@ commands, ProgressLocation } from 'vscode' import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node' import { register_abbreviations } from './abbreviations' -import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp' +import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace' import { Output_View_Provider } from './output_view' import { register_script_decorations } from './script_decorations' @@ -24,7 +24,7 @@ try { const isabelle_home = library.getenv_strict("ISABELLE_HOME") - const workspace_dir = await Isabelle_FSP.register(context) + const workspace_dir = await Isabelle_Workspace.register(context) const roots = workspace.workspaceFile === undefined ? await workspace.findFiles("{ROOT,ROOTS}") : [] const isabelle_tool = isabelle_home + "/bin/isabelle" @@ -42,13 +42,13 @@ const language_client_options: LanguageClientOptions = { documentSelector: [ - { language: "isabelle", scheme: Isabelle_FSP.scheme }, + { language: "isabelle", scheme: Isabelle_Workspace.scheme }, { language: "isabelle-ml", scheme: "file" }, { language: "bibtex", scheme: "file" } ], uriConverters: { - code2Protocol: uri => Isabelle_FSP.get_file(uri).toString(), - protocol2Code: value => Isabelle_FSP.get_isabelle(Uri.parse(value)) + code2Protocol: uri => Isabelle_Workspace.get_file(uri).toString(), + protocol2Code: value => Isabelle_Workspace.get_isabelle(Uri.parse(value)) } } @@ -98,7 +98,7 @@ } if (last_caret_update !== caret_update) { if (caret_update.uri) { - caret_update.uri = Isabelle_FSP.get_file(Uri.parse(caret_update.uri)).toString() + caret_update.uri = Isabelle_Workspace.get_file(Uri.parse(caret_update.uri)).toString() language_client.sendNotification(protocol.caret_update_type, caret_update) } last_caret_update = caret_update @@ -114,7 +114,7 @@ } if (caret_update.uri) { - caret_update.uri = Isabelle_FSP.get_isabelle(Uri.parse(caret_update.uri)).toString() + caret_update.uri = Isabelle_Workspace.get_isabelle(Uri.parse(caret_update.uri)).toString() workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document => { const editor = library.find_file_editor(document.uri) @@ -170,13 +170,13 @@ language_client.onReady().then(() => { language_client.onNotification(protocol.session_theories_type, - async ({entries}) => await Isabelle_FSP.init_workspace(entries)) + async ({entries}) => await Isabelle_Workspace.init_workspace(entries)) language_client.onNotification(protocol.symbols_type, params => { //register_abbreviations(params.entries, context) - Isabelle_FSP.update_symbol_encoder(params.entries) + Isabelle_Workspace.update_symbol_encoder(params.entries) // request theories to load in isabelle file system // after a valid symbol encoder is loaded diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts --- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts Wed Feb 23 10:46:10 2022 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,683 +0,0 @@ -'use strict'; - -import { - commands, - Disposable, - Event, - EventEmitter, - ExtensionContext, - FileChangeEvent, - FileChangeType, - FileStat, - FileSystemError, - FileSystemProvider, - FileType, - languages, - TextDocument, - Uri, ViewColumn, - window, - workspace -} from 'vscode'; -import * as path from 'path'; -import {Symbol_Encoder} from './symbol_encoder'; -import {Session_Theories, session_theories_request_type} from '../protocol'; -import {State_Key, Workspace_State} from './workspace_state'; -import * as symbol from '../symbol' -import * as library from '../library'; -import {Uri_Map} from './uri_map'; - -export class File implements FileStat -{ - type: FileType - ctime: number - mtime: number - size: number - - name: string - data?: Uint8Array - - constructor(name: string) - { - this.type = FileType.File - this.ctime = Date.now() - this.mtime = Date.now() - this.size = 0 - this.name = name - } -} - -export class Directory implements FileStat -{ - type: FileType - ctime: number - mtime: number - size: number - - name: string - entries: Map - - constructor(name: string) - { - this.type = FileType.Directory - this.ctime = Date.now() - this.mtime = Date.now() - this.size = 0 - this.name = name - this.entries = new Map() - } -} - -export type Entry = File | Directory - -export class Isabelle_FSP implements FileSystemProvider -{ - private static instance: Isabelle_FSP - private static state: Workspace_State - private static readonly draft_session = 'Draft' - private static readonly session_dir = 'Isabelle Sessions' - - //#region public static API - - public static readonly scheme = 'isabelle' - public static readonly isabelle_lang_id = 'isabelle' - public static readonly theory_extension = '.thy' - public static readonly theory_files_glob = '**/*.thy' - - public static register(context: ExtensionContext): Promise - { - this.instance = new Isabelle_FSP() - this.state = new Workspace_State(context) - context.subscriptions.push( - workspace.registerFileSystemProvider(this.scheme, this.instance), - - workspace.onDidOpenTextDocument((doc) => - this.instance.open_workspace_document(doc)), - - window.onDidChangeActiveTextEditor(({ document}) => - this.instance.active_document_dialogue(document)), - - this.instance.sync_subscription(), - - commands.registerTextEditorCommand('isabelle.reload-file', - ({document}) => this.instance.reload_document(document.uri)) - ) - - return this.instance.setup_workspace() - } - - public static async update_symbol_encoder(entries: symbol.Entry[]) - { - this.instance.symbol_encoder = new Symbol_Encoder(entries) - await this.state.set(State_Key.symbol_entries, entries) - } - - public static async init_workspace(sessions: Session_Theories[]) - { - await this.instance.init_filesystem(sessions) - for (const doc of workspace.textDocuments) { - await this.instance.open_workspace_document(doc) - } - if (window.activeTextEditor) { - await this.instance.active_document_dialogue(window.activeTextEditor.document) - } - } - - public static get_isabelle(file_uri: Uri): Uri - { - return this.instance.file_to_isabelle.get_to(file_uri) || file_uri - } - - public static get_file(isabelle_uri: Uri): Uri - { - return this.instance.file_to_isabelle.get_from(isabelle_uri) || isabelle_uri - } - - //#endregion - - - //#region subscriptions - - public async open_workspace_document(doc: TextDocument) - { - if (doc.uri.scheme === Isabelle_FSP.scheme) { - if (doc.languageId !== Isabelle_FSP.isabelle_lang_id) { - languages.setTextDocumentLanguage(doc, Isabelle_FSP.isabelle_lang_id) - } - } else { - if (doc.languageId === Isabelle_FSP.isabelle_lang_id) { - const isabelle_uri = this.file_to_isabelle.get_to(doc.uri) - if (!isabelle_uri) { - await this.create_mapping_load_theory(doc.uri) - } else if (!this.is_open_theory(isabelle_uri)) { - await this.load_theory(doc.uri, isabelle_uri) - } - } - } - } - - public async active_document_dialogue(doc: TextDocument) - { - if (doc.uri.scheme === Isabelle_FSP.scheme) { - if (!await this.is_workspace_theory(doc.uri)) { - Isabelle_FSP.warn_not_synchronized(doc.fileName) - } - } else if (doc.fileName.endsWith(Isabelle_FSP.theory_extension)) { - const isabelle_uri = this.file_to_isabelle.get_to(doc.uri) - if (!isabelle_uri || !this.is_open_theory(isabelle_uri)) { - await this.open_theory_dialogue(doc.uri) - } - } - } - - public sync_subscription(): Disposable - { - const watcher = workspace.createFileSystemWatcher(Isabelle_FSP.theory_files_glob) - watcher.onDidChange(file => this.reload_file_theory(file)) - watcher.onDidDelete(file => this._delete(this.file_to_isabelle.get_to(file))) - return watcher - } - - public async reload_document(doc: Uri) - { - if (doc.scheme === Isabelle_FSP.scheme) { - const file_uri = this.file_to_isabelle.get_from(doc) - await this.reload_theory(file_uri, doc) - } - } - - public async reload_file_theory(file_uri: Uri) - { - const isabelle_uri = this.file_to_isabelle.get_to(file_uri) - await this.reload_theory(file_uri, isabelle_uri) - } - - //#endregion - - - private symbol_encoder: Symbol_Encoder - private root = new Directory('') - private file_to_isabelle = new Uri_Map() - private session_theories: Session_Theories[] = [] - - - //#region util - - private static get_dir_uri(session: string): Uri - { - return Uri.parse(`${Isabelle_FSP.scheme}:/${session}`) - } - private static get_uri(session: string, rel_path: String): Uri - { - return Uri.parse(`${Isabelle_FSP.scheme}:/${session}/${rel_path}`) - } - - //#endregion - - - //#region initialization - - private async setup_workspace(): Promise - { - const { state } = Isabelle_FSP - let { sessions, workspace_dir, symbol_entries } = state.get_setup_data() - - const workspace_folders = workspace.workspaceFolders || [] - const isabelle_folder = workspace_folders.find(folder => - folder.name === Isabelle_FSP.session_dir && folder.uri.scheme === Isabelle_FSP.scheme) - - if (isabelle_folder === undefined) { - workspace.updateWorkspaceFolders(0, 0, - { uri: Isabelle_FSP.get_dir_uri(''), name: Isabelle_FSP.session_dir }) - } - - if (sessions && workspace_dir && symbol_entries) { - await Isabelle_FSP.update_symbol_encoder(symbol_entries) - await this.init_filesystem(sessions) - } else { - const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_FSP.scheme) - if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath - } - - await state.set(State_Key.workspace_dir, workspace_dir) - await this.save_tree_state() - this.onDidChangeFile(events => { - for (const e of events) { - if (e.type === FileChangeType.Changed) continue - - this.save_tree_state() - return - } - }) - return workspace_dir - } - - private async init_filesystem(sessions: Session_Theories[]) - { - const all_theory_uris = sessions - .map(s => s.theories) - .reduce((acc,x) => acc.concat(x), []) - - const root_entries = Array.from(this.root.entries.keys()) - - // clean old files - for (const key of root_entries) { - if (key === Isabelle_FSP.draft_session) { - const draft = this.root.entries.get(key) - - if (draft instanceof Directory) { - for (const draft_thy of draft.entries.keys()) { - const isabelle_uri = Isabelle_FSP.get_uri(Isabelle_FSP.draft_session, draft_thy) - const file_uri = this.file_to_isabelle.get_from(isabelle_uri) - - if (file_uri && all_theory_uris.includes(file_uri.toString())) { - this._delete(isabelle_uri) - } - } - } - } else { - this._delete(Isabelle_FSP.get_dir_uri(key), true) - } - } - - // create new - for (const { session_name, theories: theories_uri } of sessions) { - if (!session_name) continue - if (session_name !== Isabelle_FSP.draft_session) { - this.session_theories.push({ - session_name, - theories: theories_uri.map(t => Uri.parse(t).toString()) - }) - } - - if (!root_entries.includes(session_name)) { - this._create_directory(Isabelle_FSP.get_dir_uri(session_name)) - } - - for (const theory_uri of theories_uri) { - await this.create_mapping_load_theory(Uri.parse(theory_uri)) - } - } - } - - //#endregion - - - //#region fsp implementation - - private _emitter = new EventEmitter() - - readonly onDidChangeFile: Event = this._emitter.event - - watch(_resource: Uri): Disposable - { - // ignore, fires for all changes... - return new Disposable(() => { }) - } - - stat(uri: Uri): FileStat - { - return this._lookup(uri, false) - } - - readDirectory(uri: Uri): [string, FileType][] - { - const entry = this._lookup_directory(uri, false) - const result: [string, FileType][] = [] - for (const [name, child] of entry.entries) { - result.push([name, child.type]) - } - return result - } - - createDirectory(uri: Uri): void - { - throw FileSystemError.NoPermissions('No permission to create on Isabelle File System') - } - - readFile(uri: Uri): Uint8Array - { - const data = this._lookup_file(uri, false).data - if (data) { - return data - } - throw FileSystemError.FileNotFound() - } - - async writeFile(isabelle_uri: Uri, content: Uint8Array, options: { create: boolean, overwrite: boolean }): Promise - { - if (!this.symbol_encoder) return - if (!this.file_to_isabelle.get_from(isabelle_uri)) { - throw FileSystemError.NoPermissions('No permission to create on Isabelle File System') - } - - const basename = path.posix.basename(isabelle_uri.path) - const [parent, parent_uri] = this._get_parent_data(isabelle_uri) - let entry = parent.entries.get(basename) - if (entry instanceof Directory) { - throw FileSystemError.FileIsADirectory(isabelle_uri) - } - if (!entry && !options.create) { - throw FileSystemError.FileNotFound(isabelle_uri) - } - if (entry && options.create && !options.overwrite) { - throw FileSystemError.FileExists(isabelle_uri) - } - - if (entry) { - if (options.create) { - return this.sync_original(isabelle_uri, content) - } - - entry.mtime = Date.now() - entry.size = content.byteLength - entry.data = content - - this._fire_soon({ type: FileChangeType.Changed, uri: isabelle_uri }) - return - } - - entry = new File(basename) - entry.mtime = Date.now() - entry.size = content.byteLength - entry.data = content - - parent.entries.set(basename, entry) - parent.mtime = Date.now() - parent.size++ - this._fire_soon( - { type: FileChangeType.Changed, uri: parent_uri }, - { type: FileChangeType.Created, uri: isabelle_uri } - ) - } - - delete(uri: Uri): void - { - const [parent, parent_uri] = this._get_parent_data(uri) - if (parent && parent.name === Isabelle_FSP.draft_session) { - if (parent.size === 1) { - this._delete(parent_uri) - return - } - - this._delete(uri) - return - } - - throw FileSystemError.NoPermissions('No permission to delete on Isabelle File System') - } - - rename(oldUri: Uri, newUri: Uri, options: { overwrite: boolean }): void - { - throw FileSystemError.NoPermissions('No permission to rename on Isabelle File System') - } - - //#endregion - - - //#region implementation - - private is_open_theory(isabelle_uri: Uri): boolean - { - const open_files = workspace.textDocuments - return !!(open_files.find((doc) => doc.uri.toString() === isabelle_uri.toString())) - } - - private async load_theory(file_uri: Uri, isabelle_uri: Uri) - { - if (!this.symbol_encoder) return - const data = await workspace.fs.readFile(file_uri) - const encoded_data = this.symbol_encoder.encode(data) - await this.writeFile(isabelle_uri, encoded_data, { create: true, overwrite: true }) - } - - private async create_mapping_load_theory(file_uri: Uri): Promise - { - const session = this.get_session(file_uri) - const isabelle_uri = this.create_new_uri(file_uri, session) - this.file_to_isabelle.add(file_uri, isabelle_uri) - - await this.load_theory(file_uri, isabelle_uri) - return isabelle_uri - } - - private async is_workspace_theory(isabelle_uri: Uri): Promise - { - const file_uri = this.file_to_isabelle.get_from(isabelle_uri) - const files = await workspace.findFiles(Isabelle_FSP.theory_files_glob) - return !!(files.find(uri => uri.toString() === file_uri.toString())) - } - - private static warn_not_synchronized(file_name: string) - { - window.showWarningMessage(`Theory ${file_name} not in workspace. - Changes to underlying theory file will be overwritten.`) - } - - private async open_theory_dialogue(file_uri: Uri) - { - if (!this.symbol_encoder) return - const always_open = library.get_configuration('always_open_thys') - if (!always_open) { - const answer = await window.showInformationMessage( - 'Would you like to open the Isabelle theory associated with this file?', - 'Yes', - 'Always yes' - ) - if (answer === 'Always yes') { - library.set_configuration('always_open_thys', true) - } else if (answer !== 'Yes') { - return - } - } - - const isabelle_uri = await this.create_mapping_load_theory(file_uri) - await commands.executeCommand('vscode.open', isabelle_uri, ViewColumn.Active) - } - - private async reload_theory(file_uri: Uri, isabelle_uri: Uri) - { - if (!this.symbol_encoder) return - const data = await workspace.fs.readFile(file_uri) - const encoded_data = this.symbol_encoder.encode(data) - await this.writeFile(isabelle_uri, encoded_data, { create: false, overwrite: true }) - } - - public get_session(file_uri: Uri): string - { - let session = this.session_theories.find((s) => s.theories.includes(file_uri.toString())) - if (!session) { - if (!this.root.entries.get(Isabelle_FSP.draft_session)) { - this._create_directory(Isabelle_FSP.get_uri(Isabelle_FSP.draft_session, '')) - } - return Isabelle_FSP.draft_session - } - - return session.session_name - } - - private create_new_uri(file_uri: Uri, session_name: string): Uri - { - const file_name = path.basename(file_uri.fsPath, Isabelle_FSP.theory_extension) - let new_uri: Uri - let extra = '' - let fs_path = file_uri.fsPath - while (true) { - const discriminator = extra ? ` (${extra})` : '' - new_uri = Isabelle_FSP.get_uri(session_name, file_name + discriminator) - - const old_uri = this.file_to_isabelle.get_from(new_uri) - if (!old_uri || old_uri.toString() === file_uri.toString()) { - return new_uri - } - - if (fs_path === '/') { - throw FileSystemError.FileExists(new_uri) - } - - fs_path = path.posix.dirname(fs_path) - extra = path.posix.join(path.posix.basename(fs_path), extra) - } - } - - private async save_tree_state() - { - const sessions: Session_Theories[] = [] - for (const [session_name, val] of this.root.entries) { - if (!(val instanceof Directory)) return - const theories: string[] = [] - - for (const fileName of val.entries.keys()) { - const file = this.file_to_isabelle.get_from(Isabelle_FSP.get_uri(session_name, fileName)) - theories.push(file.toString()) - } - - sessions.push({session_name, theories}) - } - - await Isabelle_FSP.state.set(State_Key.sessions, sessions) - } - - private sync_deletion(isabelle_uri: Uri, silent: boolean) - { - const dir = this._lookup(isabelle_uri, silent) - if (!dir) { - if (silent) - return - else - throw FileSystemError.FileNotFound(isabelle_uri) - } - - const uri_string = isabelle_uri.toString() - if (dir instanceof Directory) { - for (const key of dir.entries.keys()) { - this.remove_mapping(Uri.parse(uri_string + `/${key}`)) - } - } - this.remove_mapping(isabelle_uri) - } - - private remove_mapping(isabelle_uri: Uri) - { - const file = this.file_to_isabelle.get_from(isabelle_uri) - if (file) { - this.file_to_isabelle.delete(file, isabelle_uri) - } - } - - private async sync_original(uri: Uri, content: Uint8Array) - { - if (!this.symbol_encoder) return - const origin_uri = this.file_to_isabelle.get_from(uri) - const decoded_content = this.symbol_encoder.decode(content) - workspace.fs.writeFile(origin_uri, decoded_content) - } - - private _delete(uri: Uri, silent: boolean = false): void - { - const dirname = uri.with({ path: path.posix.dirname(uri.path) }) - const basename = path.posix.basename(uri.path) - const parent = this._lookup_directory(dirname, silent) - - if (!parent) return - if (!parent.entries.has(basename)) { - if (!silent) - throw FileSystemError.FileNotFound(uri) - else - return - } - - this.sync_deletion(uri, silent) - parent.entries.delete(basename) - parent.mtime = Date.now() - parent.size -= 1 - - this._fire_soon({ type: FileChangeType.Changed, uri: dirname }, { uri, type: FileChangeType.Deleted }) - } - - private _create_directory(uri: Uri): void - { - const basename = path.posix.basename(uri.path) - const [parent, parent_uri] = this._get_parent_data(uri) - - const entry = new Directory(basename) - parent.entries.set(entry.name, entry) - parent.mtime = Date.now() - parent.size += 1 - this._fire_soon( - { type: FileChangeType.Changed, uri: parent_uri }, - { type: FileChangeType.Created, uri } - ) - } - - private _get_parent_data(uri: Uri): [Directory, Uri] - { - const parent_uri = uri.with({ path: path.posix.dirname(uri.path) }) - const parent = this._lookup_directory(parent_uri, false) - - return [parent, parent_uri] - } - - // --- lookup - - private _lookup(uri: Uri, silent: false): Entry - private _lookup(uri: Uri, silent: boolean): Entry | undefined - private _lookup(uri: Uri, silent: boolean): Entry | undefined { - const parts = uri.path.split('/') - let entry: Entry = this.root - for (const part of parts) { - if (!part) { - continue - } - let child: Entry | undefined - if (entry instanceof Directory) { - child = entry.entries.get(part) - } - if (!child) { - if (!silent) { - throw FileSystemError.FileNotFound(uri) - } else { - return undefined - } - } - entry = child - } - return entry - } - - private _lookup_directory(uri: Uri, silent: boolean): Directory - { - const entry = this._lookup(uri, silent) - if (entry instanceof Directory) { - return entry - } - throw FileSystemError.FileNotADirectory(uri) - } - - private _lookup_file(uri: Uri, silent: boolean): File - { - const entry = this._lookup(uri, silent) - if (entry instanceof File) { - return entry - } - throw FileSystemError.FileIsADirectory(uri) - } - - // --- manage file events - - private _buffered_events: FileChangeEvent[] = [] - private _fire_soon_handle?: NodeJS.Timer - - private _fire_soon(...events: FileChangeEvent[]): void - { - this._buffered_events.push(...events) - - if (this._fire_soon_handle) { - clearTimeout(this._fire_soon_handle) - } - - this._fire_soon_handle = setTimeout(() => { - this._emitter.fire(this._buffered_events) - this._buffered_events.length = 0 - }, 5) - } -} diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts Wed Feb 23 22:12:00 2022 +0100 @@ -0,0 +1,288 @@ +'use strict'; + +import * as path from 'path'; +import { + commands, + Disposable, ExtensionContext, FileChangeType, FileSystemError, languages, + TextDocument, + Uri, ViewColumn, + window, + workspace +} from 'vscode'; +import * as library from '../library'; +import { Session_Theories } from '../protocol'; +import * as symbol from '../symbol'; +import { Mapping_FSP } from './mapping_fsp'; +import { Symbol_Encoder } from './symbol_encoder'; +import { State_Key, Workspace_State } from './workspace_state'; + +export class Isabelle_Workspace +{ + private static instance: Isabelle_Workspace + private static state: Workspace_State + public static readonly draft_session = 'Draft' + private static readonly session_dir = 'Isabelle Sessions' + + private fs: Mapping_FSP + private session_theories: Session_Theories[] = [] + + public static readonly scheme = 'isabelle' + public static readonly isabelle_lang_id = 'isabelle' + public static readonly theory_extension = '.thy' + public static readonly theory_files_glob = '**/*.thy' + + public static register(context: ExtensionContext): Promise + { + this.state = new Workspace_State(context) + + const encoder = new Symbol_Encoder(this.state.get(State_Key.symbol_entries) || []) + this.instance = new Isabelle_Workspace() + this.instance.fs = new Mapping_FSP(Isabelle_Workspace.theory_files_glob, Isabelle_Workspace.scheme, encoder) + + context.subscriptions.push( + workspace.registerFileSystemProvider(this.scheme, this.instance.fs), + + workspace.onDidOpenTextDocument((doc) => + this.instance.open_workspace_document(doc)), + + window.onDidChangeActiveTextEditor(({ document}) => + this.instance.active_document_dialogue(document)), + + this.instance.fs.sync_subscription(), + + commands.registerTextEditorCommand('isabelle.reload-file', + ({document}) => this.instance.reload(document.uri)) + ) + + return this.instance.setup_workspace() + } + + public get_dir_uri(session: string): Uri + { + return Uri.parse(`${Isabelle_Workspace.scheme}:/${session}`) + } + + public get_uri(session: string, rel_path: String): Uri + { + 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 init_workspace(sessions: Session_Theories[]) + { + await this.instance.init_filesystem(sessions) + for (const doc of workspace.textDocuments) { + await this.instance.open_workspace_document(doc) + } + if (window.activeTextEditor) { + await this.instance.active_document_dialogue(window.activeTextEditor.document) + } + } + + public static get_isabelle(file_uri: Uri): Uri + { + return this.instance.fs.file_to_entry.get_to(file_uri) || file_uri + } + + public static get_file(isabelle_uri: Uri): Uri + { + return this.instance.fs.file_to_entry.get_from(isabelle_uri) || isabelle_uri + } + + public async open_workspace_document(doc: TextDocument) + { + if (doc.uri.scheme === Isabelle_Workspace.scheme) { + if (doc.languageId !== Isabelle_Workspace.isabelle_lang_id) { + languages.setTextDocumentLanguage(doc, Isabelle_Workspace.isabelle_lang_id) + } + } else { + if (doc.languageId === Isabelle_Workspace.isabelle_lang_id) { + const isabelle_uri = this.fs.file_to_entry.get_to(doc.uri) + if (!isabelle_uri) { + await this.create_mapping_load_theory(doc.uri) + } else if (!this.is_open_theory(isabelle_uri)) { + await this.fs.load(doc.uri, isabelle_uri) + } + } + } + } + + public async active_document_dialogue(doc: TextDocument) + { + if (doc.uri.scheme === Isabelle_Workspace.scheme) { + if (!await this.is_workspace_theory(doc.uri)) { + Isabelle_Workspace.warn_not_synchronized(doc.fileName) + } + } else if (doc.fileName.endsWith(Isabelle_Workspace.theory_extension)) { + const isabelle_uri = this.fs.file_to_entry.get_to(doc.uri) + if (!isabelle_uri || !this.is_open_theory(isabelle_uri)) { + await this.open_theory_dialogue(doc.uri) + } + } + } + + public async reload(doc: Uri) + { + if (doc.scheme === Isabelle_Workspace.scheme) { + const file_uri = this.fs.file_to_entry.get_from(doc) + await this.fs.reload(file_uri, doc) + } + } + + private async setup_workspace(): Promise + { + const { state } = Isabelle_Workspace + let { sessions, workspace_dir, symbol_entries } = state.get_setup_data() + + const workspace_folders = workspace.workspaceFolders || [] + const isabelle_folder = workspace_folders.find(folder => + folder.name === Isabelle_Workspace.session_dir && folder.uri.scheme === Isabelle_Workspace.scheme) + + if (isabelle_folder === undefined) { + workspace.updateWorkspaceFolders(0, 0, + { uri: Isabelle_Workspace.instance.fs.get_dir_uri(''), name: Isabelle_Workspace.session_dir }) + } + + if (sessions && workspace_dir && symbol_entries) { + await Isabelle_Workspace.update_symbol_encoder(symbol_entries) + await this.init_filesystem(sessions) + } else { + const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_Workspace.scheme) + if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath + } + + await state.set(State_Key.workspace_dir, workspace_dir) + await this.save_tree_state() + this.fs.onDidChangeFile(events => { + for (const e of events) { + if (e.type === FileChangeType.Changed) continue + + this.save_tree_state() + return + } + }) + return workspace_dir + } + + private async init_filesystem(sessions: Session_Theories[]) + { + const all_theory_uris = sessions + .map(s => s.theories) + .reduce((acc,x) => acc.concat(x), []) + + // clean old files + this.fs.clear(all_theory_uris) + + // create new + for (const { session_name, theories: theories_uri } of sessions) { + if (!session_name) continue + if (session_name !== Isabelle_Workspace.draft_session) { + this.session_theories.push({ + session_name, + theories: theories_uri.map(t => Uri.parse(t).toString()) + }) + } + + this.fs.make_dir(session_name) + + for (const theory_uri of theories_uri) { + await this.create_mapping_load_theory(Uri.parse(theory_uri)) + } + } + } + + private is_open_theory(isabelle_uri: Uri): boolean + { + const open_files = workspace.textDocuments + return !!(open_files.find((doc) => doc.uri.toString() === isabelle_uri.toString())) + } + + private async create_mapping_load_theory(file_uri: Uri): Promise + { + const session = this.get_session(file_uri) + const isabelle_uri = this.create_new_uri(file_uri, session) + this.fs.file_to_entry.add(file_uri, isabelle_uri) + + await this.fs.load(file_uri, isabelle_uri) + return isabelle_uri + } + + private async is_workspace_theory(isabelle_uri: Uri): Promise + { + const file_uri = this.fs.file_to_entry.get_from(isabelle_uri) + const files = await workspace.findFiles(Isabelle_Workspace.theory_files_glob) + return !!(files.find(uri => uri.toString() === file_uri.toString())) + } + + private static warn_not_synchronized(file_name: string) + { + window.showWarningMessage(`Theory ${file_name} not in workspace. + Changes to underlying theory file will be overwritten.`) + } + + private async open_theory_dialogue(file_uri: Uri) + { + const always_open = library.get_configuration('always_open_thys') + if (!always_open) { + const answer = await window.showInformationMessage( + 'Would you like to open the Isabelle theory associated with this file?', + 'Yes', + 'Always yes' + ) + if (answer === 'Always yes') { + library.set_configuration('always_open_thys', true) + } else if (answer !== 'Yes') { + return + } + } + + const isabelle_uri = await this.create_mapping_load_theory(file_uri) + await commands.executeCommand('vscode.open', isabelle_uri, ViewColumn.Active) + } + + + public get_session(file_uri: Uri): string + { + let session = this.session_theories.find((s) => s.theories.includes(file_uri.toString())) + if (!session) { + this.fs.make_dir(Isabelle_Workspace.draft_session) + return Isabelle_Workspace.draft_session + } + + return session.session_name + } + + private create_new_uri(file_uri: Uri, session_name: string): Uri + { + const file_name = path.basename(file_uri.fsPath, Isabelle_Workspace.theory_extension) + let new_uri: Uri + let extra = '' + let fs_path = file_uri.fsPath + while (true) { + const discriminator = extra ? ` (${extra})` : '' + new_uri = this.fs.get_uri(session_name, file_name + discriminator) + + const old_uri = this.fs.file_to_entry.get_from(new_uri) + if (!old_uri || old_uri.toString() === file_uri.toString()) { + return new_uri + } + + if (fs_path === '/') { + throw FileSystemError.FileExists(new_uri) + } + + fs_path = path.posix.dirname(fs_path) + extra = path.posix.join(path.posix.basename(fs_path), extra) + } + } + + private async save_tree_state() + { + await Isabelle_Workspace.state.set(State_Key.sessions, this.fs.get_tree_state()) + } +} diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts Wed Feb 23 22:12:00 2022 +0100 @@ -0,0 +1,436 @@ +'use strict'; + +import * as path from 'path'; +import { + Disposable, + Event, + EventEmitter, FileChangeEvent, + FileChangeType, + FileStat, + FileSystemError, + FileSystemProvider, + FileType, GlobPattern, Uri, workspace +} from 'vscode'; +import { Session_Theories } from '../protocol'; +import { Symbol_Encoder } from './symbol_encoder'; +import { Uri_Map } from './uri_map'; + + +export class File implements FileStat +{ + type: FileType + ctime: number + mtime: number + size: number + + name: string + data?: Uint8Array + + constructor(name: string) + { + this.type = FileType.File + this.ctime = Date.now() + this.mtime = Date.now() + this.size = 0 + this.name = name + } +} + + +export class Directory implements FileStat +{ + type: FileType + ctime: number + mtime: number + size: number + + name: string + entries: Map + + constructor(name: string) + { + this.type = FileType.Directory + this.ctime = Date.now() + this.mtime = Date.now() + this.size = 0 + this.name = name + this.entries = new Map() + } +} + + +export type Entry = File | Directory + + +export class Mapping_FSP implements FileSystemProvider +{ + private root = new Directory('') + file_to_entry = new Uri_Map() + private symbol_encoder: Symbol_Encoder + private readonly scheme: string + private readonly glob: GlobPattern + + constructor(glob: GlobPattern, scheme: string, encoder: Symbol_Encoder) + { + this.scheme = scheme + this.symbol_encoder = encoder + } + + public update_symbol_encoder(encoder: Symbol_Encoder) + { + this.symbol_encoder = encoder + } + + public sync_subscription(): Disposable + { + const watcher = workspace.createFileSystemWatcher(this.glob) + watcher.onDidChange(file => { + const entry = this.file_to_entry.get_to(file) + if (entry) this.reload(file, entry) + }) + watcher.onDidDelete(file => this._delete(this.file_to_entry.get_to(file))) + return watcher + } + + private async sync_original(uri: Uri, content: Uint8Array) + { + const origin_uri = this.file_to_entry.get_from(uri) + const decoded_content = this.symbol_encoder.decode(content) + workspace.fs.writeFile(origin_uri, decoded_content) + } + + public get_dir_uri(session: string): Uri + { + return Uri.parse(`${this.scheme}:/${session}`) + } + + public get_uri(session: string, rel_path: String): Uri + { + return Uri.parse(`${this.scheme}:/${session}/${rel_path}`) + } + + + // #region create + + private _create_directory(uri: Uri): void + { + const basename = path.posix.basename(uri.path) + const [parent, parent_uri] = this._get_parent_data(uri) + + const entry = new Directory(basename) + parent.entries.set(entry.name, entry) + parent.mtime = Date.now() + parent.size += 1 + this._fire_soon( + { type: FileChangeType.Changed, uri: parent_uri }, + { type: FileChangeType.Created, uri } + ) + } + + public make_dir(name: string) + { + const root_entries = Array.from(this.root.entries.keys()) + + if (!root_entries.includes(name)) { + this._create_directory(this.get_dir_uri(name)) + } + } + + // #endregion + + + // #region read + + public async load(file_uri: Uri, isabelle_uri: Uri) + { + const data = await workspace.fs.readFile(file_uri) + const encoded_data = this.symbol_encoder.encode(data) + await this.writeFile(isabelle_uri, encoded_data, { create: true, overwrite: true }) + } + + public async reload(file_uri: Uri, isabelle_uri: Uri) + { + const data = await workspace.fs.readFile(file_uri) + const encoded_data = this.symbol_encoder.encode(data) + await this.writeFile(isabelle_uri, encoded_data, { create: false, overwrite: true }) + } + + // #endregion + + + // #region delete + + _delete(uri: Uri, silent: boolean = false): void + { + const dirname = uri.with({ path: path.posix.dirname(uri.path) }) + const basename = path.posix.basename(uri.path) + const parent = this._lookup_directory(dirname, silent) + + if (!parent) return + if (!parent.entries.has(basename)) { + if (!silent) + throw FileSystemError.FileNotFound(uri) + else + return + } + + this.sync_deletion(uri, silent) + parent.entries.delete(basename) + parent.mtime = Date.now() + parent.size -= 1 + + this._fire_soon({ type: FileChangeType.Changed, uri: dirname }, { uri, type: FileChangeType.Deleted }) + } + + private sync_deletion(isabelle_uri: Uri, silent: boolean) + { + const dir = this._lookup(isabelle_uri, silent) + if (!dir) { + if (silent) + return + else + throw FileSystemError.FileNotFound(isabelle_uri) + } + + const uri_string = isabelle_uri.toString() + if (dir instanceof Directory) { + for (const key of dir.entries.keys()) { + this.remove_mapping(Uri.parse(uri_string + `/${key}`)) + } + } + this.remove_mapping(isabelle_uri) + } + + private remove_mapping(isabelle_uri: Uri) + { + const file = this.file_to_entry.get_from(isabelle_uri) + if (file) { + this.file_to_entry.delete(file, isabelle_uri) + } + } + + public clear(all_theory_uris: string[]) + { + const root_entries = Array.from(this.root.entries.keys()) + + for (const key of root_entries) { + if (key === 'Draft') { + const draft = this.root.entries.get(key) + + if (draft instanceof Directory) { + for (const draft_thy of draft.entries.keys()) { + const isabelle_uri = this.get_uri('Draft', draft_thy) + const file_uri = this.file_to_entry.get_from(isabelle_uri) + + if (file_uri && all_theory_uris.includes(file_uri.toString())) { + this._delete(isabelle_uri) + } + } + } + } else { + this._delete(this.get_dir_uri(key), true) + } + } + } + + // #endregion + + private _get_parent_data(uri: Uri): [Directory, Uri] + { + const parent_uri = uri.with({ path: path.posix.dirname(uri.path) }) + const parent = this._lookup_directory(parent_uri, false) + + return [parent, parent_uri] + } + + private _lookup(uri: Uri, silent: false): Entry + private _lookup(uri: Uri, silent: boolean): Entry | undefined + private _lookup(uri: Uri, silent: boolean): Entry | undefined { + const parts = uri.path.split('/') + let entry: Entry = this.root + for (const part of parts) { + if (!part) { + continue + } + let child: Entry | undefined + if (entry instanceof Directory) { + child = entry.entries.get(part) + } + if (!child) { + if (!silent) { + throw FileSystemError.FileNotFound(uri) + } else { + return undefined + } + } + entry = child + } + return entry + } + + private _lookup_directory(uri: Uri, silent: boolean): Directory + { + const entry = this._lookup(uri, silent) + if (entry instanceof Directory) { + return entry + } + throw FileSystemError.FileNotADirectory(uri) + } + + private _lookup_file(uri: Uri, silent: boolean): File + { + const entry = this._lookup(uri, silent) + if (entry instanceof File) { + return entry + } + throw FileSystemError.FileIsADirectory(uri) + } + + public get_tree_state(): Session_Theories[] + { + const sessions: Session_Theories[] = [] + for (const [session_name, val] of this.root.entries) { + if (!(val instanceof Directory)) return + const theories: string[] = [] + + for (const fileName of val.entries.keys()) { + const file = this.file_to_entry.get_from(this.get_uri(session_name, fileName)) + theories.push(file.toString()) + } + + sessions.push({session_name, theories}) + } + return sessions + } + + + //#region events + + private _buffered_events: FileChangeEvent[] = [] + private _fire_soon_handle?: NodeJS.Timer + + private _fire_soon(...events: FileChangeEvent[]): void + { + this._buffered_events.push(...events) + + if (this._fire_soon_handle) { + clearTimeout(this._fire_soon_handle) + } + + this._fire_soon_handle = setTimeout(() => { + this._emitter.fire(this._buffered_events) + this._buffered_events.length = 0 + }, 5) + } + + private _emitter = new EventEmitter() + + //#endregion + + + //#region fsp implementation + + readonly onDidChangeFile: Event = this._emitter.event + + watch(_resource: Uri): Disposable + { + return new Disposable(() => { }) + } + + stat(uri: Uri): FileStat + { + return this._lookup(uri, false) + } + + readDirectory(uri: Uri): [string, FileType][] + { + const entry = this._lookup_directory(uri, false) + const result: [string, FileType][] = [] + for (const [name, child] of entry.entries) { + result.push([name, child.type]) + } + return result + } + + createDirectory(uri: Uri): void + { + throw FileSystemError.NoPermissions('No permission to create on Isabelle File System') + } + + readFile(uri: Uri): Uint8Array + { + const data = this._lookup_file(uri, false).data + if (data) { + return data + } + throw FileSystemError.FileNotFound() + } + + async writeFile(isabelle_uri: Uri, content: Uint8Array, options: { create: boolean, overwrite: boolean }): Promise + { + if (!this.file_to_entry.get_from(isabelle_uri)) { + throw FileSystemError.NoPermissions('No permission to create on Isabelle File System') + } + + const basename = path.posix.basename(isabelle_uri.path) + const [parent, parent_uri] = this._get_parent_data(isabelle_uri) + let entry = parent.entries.get(basename) + if (entry instanceof Directory) { + throw FileSystemError.FileIsADirectory(isabelle_uri) + } + if (!entry && !options.create) { + throw FileSystemError.FileNotFound(isabelle_uri) + } + if (entry && options.create && !options.overwrite) { + throw FileSystemError.FileExists(isabelle_uri) + } + + if (entry) { + if (options.create) { + return this.sync_original(isabelle_uri, content) + } + + entry.mtime = Date.now() + entry.size = content.byteLength + entry.data = content + + this._fire_soon({ type: FileChangeType.Changed, uri: isabelle_uri }) + return + } + + entry = new File(basename) + entry.mtime = Date.now() + entry.size = content.byteLength + entry.data = content + + parent.entries.set(basename, entry) + parent.mtime = Date.now() + parent.size++ + this._fire_soon( + { type: FileChangeType.Changed, uri: parent_uri }, + { type: FileChangeType.Created, uri: isabelle_uri } + ) + } + + delete(uri: Uri): void + { + const [parent, parent_uri] = this._get_parent_data(uri) + if (parent && parent.name === 'Draft') { + if (parent.size === 1) { + this._delete(parent_uri) + return + } + + this._delete(uri) + return + } + + throw FileSystemError.NoPermissions('No permission to delete on Isabelle File System') + } + + rename(oldUri: Uri, newUri: Uri, options: { overwrite: boolean }): void + { + throw FileSystemError.NoPermissions('No permission to rename on Isabelle File System') + } + // #endregion +} \ No newline at end of file diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/library.ts --- a/src/Tools/VSCode/extension/src/library.ts Wed Feb 23 10:46:10 2022 +0100 +++ b/src/Tools/VSCode/extension/src/library.ts Wed Feb 23 22:12:00 2022 +0100 @@ -2,7 +2,7 @@ import * as os from 'os' import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode' -import {Isabelle_FSP} from './isabelle_filesystem/isabelle_fsp' +import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace' /* regular expressions */ @@ -58,7 +58,7 @@ export function is_file(uri: Uri): boolean { - return uri.scheme === "file" || uri.scheme === Isabelle_FSP.scheme + return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme } export function find_file_editor(uri: Uri): TextEditor | undefined diff -r c04ccea8bdd2 -r 8dd7f0130266 src/Tools/VSCode/extension/src/output_view.ts --- a/src/Tools/VSCode/extension/src/output_view.ts Wed Feb 23 10:46:10 2022 +0100 +++ b/src/Tools/VSCode/extension/src/output_view.ts Wed Feb 23 22:12:00 2022 +0100 @@ -5,7 +5,7 @@ import { text_colors } from './decorations' import * as library from './library' import * as path from 'path' -import { Isabelle_FSP } from './isabelle_filesystem/isabelle_fsp' +import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace' class Output_View_Provider implements WebviewViewProvider { @@ -64,7 +64,7 @@ const line = Number(uri.fragment) || 0 const pos = new Position(line, 0) const uri_no_fragment = uri.with({ fragment: '' }) - const isabelle_uri = Isabelle_FSP.get_isabelle(uri_no_fragment) + const isabelle_uri = Isabelle_Workspace.get_isabelle(uri_no_fragment) window.showTextDocument(isabelle_uri, { preserveFocus: false, selection: new Selection(pos, pos)