diff --git a/src/Tools/VSCode/extension/src/extension.ts b/src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts +++ b/src/Tools/VSCode/extension/src/extension.ts @@ -1,219 +1,219 @@ 'use strict'; import * as path from 'path' import * as library from './library' import * as decorations from './decorations' import * as preview_panel from './preview_panel' import * as protocol from './protocol' import * as state_panel from './state_panel' import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window, commands, ProgressLocation } from 'vscode' import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node' import { register_abbreviations } from './abbreviations' import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace' import { Output_View_Provider } from './output_view' import { register_script_decorations } from './script_decorations' let last_caret_update: protocol.Caret_Update = {} export async function activate(context: ExtensionContext) { /* server */ try { const isabelle_home = library.getenv_strict("ISABELLE_HOME") 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" const isabelle_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] .concat(library.get_configuration>("args")) .concat(roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : []) const server_options: ServerOptions = library.platform_is_windows() ? { command: library.getenv_strict("CYGWIN_ROOT") + "\\bin\\bash", args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } : { command: isabelle_tool, args: ["vscode_server"].concat(isabelle_args) } const language_client_options: LanguageClientOptions = { documentSelector: [ { language: "isabelle", scheme: Isabelle_Workspace.scheme }, { language: "isabelle-ml", scheme: "file" }, { language: "bibtex", scheme: "file" } ], uriConverters: { code2Protocol: uri => Isabelle_Workspace.get_file(uri).toString(), protocol2Code: value => Isabelle_Workspace.get_isabelle(Uri.parse(value)) } } const language_client = new LanguageClient("Isabelle", server_options, language_client_options, false) window.withProgress({location: ProgressLocation.Notification, cancellable: false}, async (progress) => { progress.report({ message: "Waiting for Isabelle server..." }) await language_client.onReady() }) /* decorations */ decorations.setup(context) context.subscriptions.push( workspace.onDidChangeConfiguration(() => decorations.setup(context)), workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)), window.onDidChangeActiveTextEditor(decorations.update_editor), workspace.onDidCloseTextDocument(decorations.close_document)) language_client.onReady().then(() => language_client.onNotification(protocol.decoration_type, decorations.apply_decoration)) /* super-/subscript decorations */ register_script_decorations(context) /* caret handling */ function update_caret() { const editor = window.activeTextEditor let caret_update: protocol.Caret_Update = {} if (editor) { const uri = editor.document.uri const cursor = editor.selection.active if (library.is_file(uri) && cursor) caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character } } if (last_caret_update !== caret_update) { if (caret_update.uri) { 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 } } function goto_file(caret_update: protocol.Caret_Update) { function move_cursor(editor: TextEditor) { const pos = new Position(caret_update.line || 0, caret_update.character || 0) editor.selections = [new Selection(pos, pos)] } if (caret_update.uri) { 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) const column = editor ? editor.viewColumn : ViewColumn.One window.showTextDocument(document, column, !caret_update.focus).then(move_cursor) }) } } language_client.onReady().then(() => { context.subscriptions.push( window.onDidChangeActiveTextEditor(_ => update_caret()), window.onDidChangeTextEditorSelection(_ => update_caret())) update_caret() language_client.onNotification(protocol.caret_update_type, goto_file) }) /* dynamic output */ const provider = new Output_View_Provider(context.extensionUri) context.subscriptions.push( window.registerWebviewViewProvider(Output_View_Provider.view_type, provider)) language_client.onReady().then(() => { language_client.onNotification(protocol.dynamic_output_type, params => provider.update_content(params.content)) }) /* state panel */ context.subscriptions.push( commands.registerCommand("isabelle.state", uri => state_panel.init(uri))) language_client.onReady().then(() => state_panel.setup(context, language_client)) /* preview panel */ context.subscriptions.push( commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)), commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true))) language_client.onReady().then(() => preview_panel.setup(context, language_client)) /* Isabelle symbols and abbreviations */ language_client.onReady().then(() => { language_client.onNotification(protocol.session_theories_type, - async ({entries}) => await Isabelle_Workspace.init_workspace(entries)) + async ({entries}) => await Isabelle_Workspace.update_sessions(entries)) language_client.onNotification(protocol.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(protocol.session_theories_request_type) }) language_client.sendNotification(protocol.symbols_request_type) }) /* spell checker */ language_client.onReady().then(() => { context.subscriptions.push( commands.registerCommand("isabelle.include-word", uri => language_client.sendNotification(protocol.include_word_type)), commands.registerCommand("isabelle.include-word-permanently", uri => language_client.sendNotification(protocol.include_word_permanently_type)), commands.registerCommand("isabelle.exclude-word", uri => language_client.sendNotification(protocol.exclude_word_type)), commands.registerCommand("isabelle.exclude-word-permanently", uri => language_client.sendNotification(protocol.exclude_word_permanently_type)), commands.registerCommand("isabelle.reset-words", uri => language_client.sendNotification(protocol.reset_words_type))) }) /* start server */ context.subscriptions.push(language_client.start()) } catch (exn) { window.showErrorMessage(exn) } } export function deactivate() { } diff --git a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts --- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts +++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts @@ -1,288 +1,270 @@ '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[]) + public static async update_sessions(sessions: Session_Theories[]) { - await this.instance.init_filesystem(sessions) + await Isabelle_Workspace.state.set(State_Key.sessions, sessions) + await this.instance.load_tree_state(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 + return this.instance.fs.get_entry(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 + return this.instance.fs.get_file(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) + const isabelle_uri = this.fs.get_entry(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) + await this.fs.reload(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) + const isabelle_uri = this.fs.get_entry(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) + const file_uri = this.fs.get_file(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 }) + { 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) - await this.init_filesystem(sessions) + await this.load_tree_state(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[]) + private async load_tree_state(sessions: Session_Theories[]) { - const all_theory_uris = sessions - .map(s => s.theories) - .reduce((acc,x) => acc.concat(x), []) + const root_entries = this.fs.list_dirs(this.get_dir_uri('')) + for (const key of root_entries) { + this.fs.remove(this.get_dir_uri(key)) + } - // 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) + this.fs.make_dir(this.get_dir_uri(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 file_uri = this.fs.get_file(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) + this.fs.make_dir(this.get_dir_uri(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) + new_uri = this.get_uri(session_name, file_name + discriminator) - const old_uri = this.fs.file_to_entry.get_from(new_uri) + const old_uri = this.fs.get_file(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()) - } -} +} \ No newline at end of file diff --git a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts --- a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts +++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts @@ -1,436 +1,402 @@ '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 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.glob = glob 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))) + watcher.onDidDelete(file => this.remove(this.file_to_entry.get_to(file), true)) return watcher } - private async sync_original(uri: Uri, content: Uint8Array) + + public get_entry(file: Uri): Uri | undefined { - 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}`) + return this.file_to_entry.get_to(file) } - public get_uri(session: string, rel_path: String): Uri + public get_file(entry: Uri): Uri | undefined { - return Uri.parse(`${this.scheme}:/${session}/${rel_path}`) + return this.file_to_entry.get_from(entry) } - - // #region create - - private _create_directory(uri: Uri): void + + 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 list_dirs(uri: Uri): string[] + { + const res: string[] = [] + for (const [name, dir] of this.lookup_directory(uri, false).entries) { + if (dir instanceof Directory) { + res.push(dir.name) + } + } + + return res + } + + public list_files(uri: Uri): string[] + { + const res: string[] = [] + for (const [name, dir] of this.lookup_directory(uri, false).entries) { + if (dir instanceof File) { + res.push(dir.name) + } + } + + return res + } + + + public make_dir(uri: Uri): void { const basename = path.posix.basename(uri.path) - const [parent, parent_uri] = this._get_parent_data(uri) + 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)) + if (!parent.entries.has(basename)) { + 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 } + ) } } - // #endregion - - - // #region read public async load(file_uri: Uri, isabelle_uri: Uri) { + this.file_to_entry.add(file_uri, isabelle_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 + 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) + } - // #region delete - - _delete(uri: Uri, silent: boolean = false): void + remove(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) + 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 }) + 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) + 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 buffered_events: FileChangeEvent[] = [] + private fire_soon_handle?: NodeJS.Timer - 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 + private fire_soon(...events: FileChangeEvent[]): void { - 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[] = [] + this.buffered_events.push(...events) - 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) + 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 + this.fire_soon_handle = setTimeout(() => { + this.emitter.fire(this.buffered_events) + this.buffered_events.length = 0 }, 5) } - private _emitter = new EventEmitter() - - //#endregion + private emitter = new EventEmitter() //#region fsp implementation - readonly onDidChangeFile: Event = this._emitter.event + readonly onDidChangeFile: Event = this.emitter.event watch(_resource: Uri): Disposable { return new Disposable(() => { }) } stat(uri: Uri): FileStat { - return this._lookup(uri, false) + return this.lookup(uri, false) } readDirectory(uri: Uri): [string, FileType][] { - const entry = this._lookup_directory(uri, false) + 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 + 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) + 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 }) + 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( + 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) + const [parent, parent_uri] = this.get_parent_data(uri) if (parent && parent.name === 'Draft') { if (parent.size === 1) { - this._delete(parent_uri) + this.remove(parent_uri) return } - this._delete(uri) + this.remove(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