--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts Wed Feb 23 22:12:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts Wed Feb 23 23:17:39 2022 +0100
@@ -73,9 +73,10 @@
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)
}
@@ -86,12 +87,12 @@
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)
@@ -102,11 +103,11 @@
}
} 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)
}
}
}
@@ -119,7 +120,7 @@
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)
}
@@ -129,7 +130,7 @@
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)
}
}
@@ -145,40 +146,28 @@
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) {
@@ -188,7 +177,7 @@
})
}
- 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))
@@ -206,15 +195,13 @@
{
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<boolean>
{
- 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()))
}
@@ -250,7 +237,7 @@
{
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
}
@@ -265,9 +252,9 @@
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
}
@@ -280,9 +267,4 @@
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
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts Wed Feb 23 22:12:00 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts Wed Feb 23 23:17:39 2022 +0100
@@ -65,17 +65,20 @@
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
@@ -88,61 +91,119 @@
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
+ {
+ return this.file_to_entry.get_to(file)
+ }
+
+ public get_file(entry: 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)
+ return this.file_to_entry.get_from(entry)
+ }
+
+
+ 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]
}
- public get_dir_uri(session: string): Uri
- {
- return Uri.parse(`${this.scheme}:/${session}`)
+ 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
}
- public get_uri(session: string, rel_path: String): Uri
+ private lookup_directory(uri: Uri, silent: boolean): Directory
{
- return Uri.parse(`${this.scheme}:/${session}/${rel_path}`)
+ 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
+ }
- // #region create
-
- private _create_directory(uri: Uri): void
+ 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 })
@@ -155,16 +216,19 @@
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)) {
@@ -179,12 +243,12 @@
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
@@ -209,128 +273,30 @@
}
}
- 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 buffered_events: FileChangeEvent[] = []
+ private fire_soon_handle?: NodeJS.Timer
- 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
+ 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<FileChangeEvent[]>()
-
- //#endregion
+ private emitter = new EventEmitter<FileChangeEvent[]>()
//#region fsp implementation
- readonly onDidChangeFile: Event<FileChangeEvent[]> = this._emitter.event
+ readonly onDidChangeFile: Event<FileChangeEvent[]> = this.emitter.event
watch(_resource: Uri): Disposable
{
@@ -339,12 +305,12 @@
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])
@@ -359,7 +325,7 @@
readFile(uri: Uri): Uint8Array
{
- const data = this._lookup_file(uri, false).data
+ const data = this.lookup_file(uri, false).data
if (data) {
return data
}
@@ -373,7 +339,7 @@
}
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)
@@ -394,7 +360,7 @@
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
}
@@ -406,7 +372,7 @@
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 }
)
@@ -414,14 +380,14 @@
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
}