discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
discontinued special treatment of workspace_dir as session directory;
--- a/src/Tools/VSCode/extension/package.json Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/package.json Fri Mar 11 12:56:37 2022 +0100
@@ -208,11 +208,6 @@
],
"description": "Symbol replacement mode."
},
- "isabelle.always_open_thys": {
- "type": "boolean",
- "default": false,
- "description": "Always open '.thy' files as Isabelle theories."
- },
"isabelle.text_color": {
"type": "object",
"additionalProperties": {
--- a/src/Tools/VSCode/extension/src/abbreviations.ts Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/abbreviations.ts Fri Mar 11 12:56:37 2022 +0100
@@ -6,7 +6,7 @@
'use strict';
import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode'
-import { Prefix_Tree } from './isabelle_filesystem/prefix_tree'
+import { Prefix_Tree } from './prefix_tree'
import * as library from './library'
import * as vscode_lib from './vscode_lib'
import * as symbol from './symbol'
--- a/src/Tools/VSCode/extension/src/decorations.ts Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Fri Mar 11 12:56:37 2022 +0100
@@ -11,7 +11,6 @@
TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode'
import { Document_Decorations } from './lsp'
import * as vscode_lib from './vscode_lib'
-import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace'
/* known decoration types */
@@ -174,7 +173,7 @@
export function apply_decoration(decorations: Document_Decorations)
{
- const uri = Isabelle_Workspace.get_isabelle(Uri.parse(decorations.uri))
+ const uri = Uri.parse(decorations.uri)
for (const decoration of decorations.entries) {
const typ = types.get(decoration.type)
--- a/src/Tools/VSCode/extension/src/extension.ts Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Fri Mar 11 12:56:37 2022 +0100
@@ -19,7 +19,6 @@
import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window,
commands, ProgressLocation } from 'vscode'
import { LanguageClient, LanguageClientOptions, ServerOptions } from 'vscode-languageclient/node'
-import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace'
import { Output_View_Provider } from './output_view'
import { register_script_decorations } from './script_decorations'
@@ -32,15 +31,10 @@
try {
const isabelle_home = library.getenv_strict("ISABELLE_HOME")
-
- const workspace_dir = await Isabelle_Workspace.register(context, symbol.symbols)
- 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(vscode_lib.get_configuration<Array<string>>("args"))
- .concat(roots.length > 0 && workspace_dir ? ["-D", file.standard_path(workspace_dir)] : [])
const server_options: ServerOptions =
platform.is_windows() ?
@@ -51,14 +45,10 @@
const language_client_options: LanguageClientOptions = {
documentSelector: [
- { language: "isabelle", scheme: Isabelle_Workspace.scheme },
+ { language: "isabelle", scheme: "file" },
{ 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 =
@@ -107,7 +97,6 @@
}
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(lsp.caret_update_type, caret_update)
}
last_caret_update = caret_update
@@ -123,7 +112,6 @@
}
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 = vscode_lib.find_file_editor(document.uri)
@@ -174,17 +162,6 @@
language_client.onReady().then(() => preview_panel.setup(context, language_client))
- /* Isabelle symbols and abbreviations */
-
- language_client.onReady().then(() =>
- {
- language_client.onNotification(lsp.session_theories_type,
- async ({entries}) => await Isabelle_Workspace.update_sessions(entries))
-
- language_client.sendNotification(lsp.session_theories_request_type)
- })
-
-
/* spell checker */
language_client.onReady().then(() =>
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts Thu Mar 10 20:16:19 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,268 +0,0 @@
-/* Author: Denis Paluca and Fabian Huch, TU Muenchen
-
-Handling of theory files in VSCode workspace.
-*/
-
-'use strict';
-
-import * as path from 'path';
-import {
- commands,
- ExtensionContext, FileSystemError, languages, TextDocument,
- Uri, ViewColumn,
- window,
- workspace
-} from 'vscode';
-import * as vscode_lib from '../vscode_lib';
-import { Session_Theories } from '../lsp';
-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, symbols: symbol.Symbols): Promise<string|undefined>
- {
- this.state = new Workspace_State(context)
-
- 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)
-
- 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_sessions(sessions: Session_Theories[])
- {
- 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.get_entry(file_uri) || file_uri
- }
-
- public static get_file(isabelle_uri: Uri): 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.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.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.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.get_file(doc)
- await this.fs.reload(file_uri, doc)
- }
- }
-
- private async setup_workspace(): Promise<string|undefined>
- {
- const { state } = Isabelle_Workspace
- let { sessions, workspace_dir } = 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.get_dir_uri(''), name: Isabelle_Workspace.session_dir })
- }
-
- if (sessions && workspace_dir) {
- 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)
- return workspace_dir
- }
-
- private async load_tree_state(sessions: Session_Theories[])
- {
- 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))
- }
-
- 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(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<Uri>
- {
- const session = this.get_session(file_uri)
- const isabelle_uri = this.create_new_uri(file_uri, session)
- 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.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 = vscode_lib.get_configuration<boolean>('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') {
- vscode_lib.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(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.get_uri(session_name, file_name + discriminator)
-
- 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)
- }
- }
-}
\ No newline at end of file
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts Thu Mar 10 20:16:19 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,401 +0,0 @@
-/* Author: Denis Paluca and Fabian Huch, TU Muenchen
-
-Memory-mapped virtual filesystem with symbol encoding.
-*/
-
-'use strict';
-
-import * as path from 'path';
-import {
- Disposable,
- Event,
- EventEmitter, FileChangeEvent,
- FileChangeType,
- FileStat,
- FileSystemError,
- FileSystemProvider,
- FileType, GlobPattern, Uri, workspace
-} from 'vscode';
-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<string, File | Directory>
-
- 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('')
- 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 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.remove(this.file_to_entry.get_to(file), true))
- return watcher
- }
-
-
- public get_entry(file: Uri): Uri | undefined
- {
- return this.file_to_entry.get_to(file)
- }
-
- public get_file(entry: Uri): Uri | undefined
- {
- 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]
- }
-
- 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)
-
- 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 }
- )
- }
- }
-
-
- 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 })
- }
-
- 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)
- }
-
-
- 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)
-
- 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)
- }
- }
-
-
- 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<FileChangeEvent[]>()
-
-
- //#region fsp implementation
-
- readonly onDidChangeFile: Event<FileChangeEvent[]> = 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<void>
- {
- 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.remove(parent_uri)
- return
- }
-
- 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
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts Thu Mar 10 20:16:19 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-/* Author: Denis Paluca, TU Muenchen
-
-Prefix tree for symbol autocompletion.
-*/
-
-'use strict';
-
-class Tree_Node
-{
- public key: number | string
- public parent: Tree_Node = null
- public end: boolean = false
- public value: number[] | string
- public children: Record<number | string, Tree_Node> = {}
- constructor(key: number | string)
- {
- this.key = key
- }
-
- public get_word(): number[] | string[]
- {
- let output = []
- let node: Tree_Node = this
-
- while (node.key !== null) {
- output.unshift(node.key)
- node = node.parent
- }
-
- return output
- }
-}
-
-class Prefix_Tree
-{
- private root: Tree_Node
-
- constructor()
- {
- this.root = new Tree_Node(null)
- }
-
- public insert(word: number[] | string, value: number[] | string)
- {
- let node = this.root
- for (var i = 0; i < word.length; i++) {
- if (!node.children[word[i]]) {
- node.children[word[i]] = new Tree_Node(word[i])
-
- node.children[word[i]].parent = node
- }
-
- node = node.children[word[i]]
- node.end = false
-
- if (i === word.length-1) {
- node.end = true
- node.value = value
- }
- }
- }
-
- public get_node(prefix: number[] | string): Tree_Node | undefined
- {
- let node = this.root
-
- for (let i = 0; i < prefix.length; i++) {
- if (!node.children[prefix[i]]) {
- return
- }
- node = node.children[prefix[i]]
- }
- return node
- }
-
- public get_end_or_value(prefix: number[] | string): Tree_Node | undefined
- {
- let node = this.root
- let resNode: Tree_Node
- for (let i = 0; i < prefix.length; i++) {
- if (!node.children[prefix[i]]) {
- return resNode
- }
- node = node.children[prefix[i]]
- if (node.value) {
- resNode = node
- }
-
- if (node.end) {
- return node
- }
- }
- return node
- }
-}
-
-export { Prefix_Tree, Tree_Node }
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts Thu Mar 10 20:16:19 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-/* Author: Denis Paluca, TU Muenchen
-
-Encoding of Isabelle symbols.
-*/
-
-'use strict';
-
-import { TextEncoder } from 'util'
-import * as symbol from '../symbol'
-import { Prefix_Tree, Tree_Node } from './prefix_tree'
-
-class Encode_Data
-{
- prefix_tree: Prefix_Tree
- min_length: number
- max_length: number
-
- constructor(origin: Uint8Array[], replacement: Uint8Array[])
- {
- this.prefix_tree = new Prefix_Tree()
-
- for (let i = 0; i < origin.length; i++) {
- const entry = origin[i]
- if (!this.min_length || this.min_length > entry.length)
- this.min_length = entry.length
-
- if (!this.max_length || this.max_length< entry.length)
- this.max_length = entry.length
-
- this.prefix_tree.insert(Array.from(entry), Array.from(replacement[i]))
- }
- }
-}
-
-export class Symbol_Encoder
-{
- private symbols: Encode_Data
- private sequences: Encode_Data
-
- constructor(entries: symbol.Entry[])
- {
- let syms: Uint8Array[] = []
- let seqs: Uint8Array[] = []
- const encoder = new TextEncoder()
- for (const {symbol, code} of entries) {
- seqs.push(encoder.encode(symbol))
- syms.push(encoder.encode(String.fromCharCode(code)))
- }
- this.symbols = new Encode_Data(syms, seqs)
- this.sequences = new Encode_Data(seqs, syms)
- }
-
- encode(content: Uint8Array): Uint8Array
- {
- return this.code(content, this.sequences, this.symbols)
- }
-
- decode(content: Uint8Array): Uint8Array
- {
- return this.code(content, this.symbols, this.sequences)
- }
-
- private code(content: Uint8Array, origin: Encode_Data, replacements: Encode_Data): Uint8Array
- {
- const result: number[] = []
-
- for (let i = 0; i < content.length; i++) {
- if (i > content.length - origin.min_length) {
- result.push(content[i])
- continue
- }
-
- let word: number[] = []
- let node: Tree_Node
- for (let j = i; j < i + origin.max_length; j++) {
- word.push(content[j])
- node = origin.prefix_tree.get_node(word)
- if (!node || node.end) {
- break
- }
- }
-
- if (node && node.end) {
- result.push(...(node.value as number[]))
- i += word.length - 1
- continue
- }
- result.push(content[i])
- }
-
- return new Uint8Array(result)
- }
-}
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts Thu Mar 10 20:16:19 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-/* Author: Fabian Huch, TU Muenchen
-
-Bidirectional mapping between uris.
-*/
-
-'use strict';
-
-import {Uri} from 'vscode';
-
-export class Uri_Map
-{
- private map = new Map<string, Uri>()
- private rev_map = new Map<string, Uri>()
-
- private static normalize(uri: Uri): Uri
- {
- return Uri.parse(uri.toString())
- }
-
- public keys(): Uri[]
- {
- return [...this.rev_map.values()]
- }
-
- public add(from: Uri, to: Uri)
- {
- const norm_from = Uri_Map.normalize(from)
- const norm_to = Uri_Map.normalize(to)
- this.map.set(norm_from.toString(), norm_to)
- this.rev_map.set(norm_to.toString(), norm_from)
- }
-
- public delete(from: Uri, to: Uri)
- {
- this.map.delete(Uri_Map.normalize(from).toString())
- this.rev_map.delete(Uri_Map.normalize(to).toString())
- }
-
- public get_to(from: Uri): Uri
- {
- return this.map.get(Uri_Map.normalize(from).toString())
- }
-
- public get_from(to: Uri): Uri
- {
- return this.rev_map.get(Uri_Map.normalize(to).toString())
- }
-}
\ No newline at end of file
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts Thu Mar 10 20:16:19 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-/* Author: Denis Paluca and Fabian Huch, TU Muenchen
-
-Persistent workspace state.
-*/
-
-'use strict';
-
-import { ExtensionContext } from 'vscode'
-import { Session_Theories } from '../lsp'
-import * as symbol from '../symbol'
-
-interface Setup_Data
-{
- workspace_dir: string
- sessions: Session_Theories[]
-}
-
-enum State_Key
-{
- workspace_dir = 'workspace_dir',
- sessions = 'sessions'
-}
-
-class Workspace_State
-{
- constructor(private context: ExtensionContext) { }
-
- public get_setup_data(): Setup_Data
- {
- return {
- workspace_dir: this.get(State_Key.workspace_dir),
- sessions: this.get<Session_Theories[]>(State_Key.sessions)
- }
- }
-
- public set_setup_date(setup_data: Setup_Data)
- {
- const {workspace_dir: workspace_dir, sessions } = setup_data
- this.set(State_Key.workspace_dir, workspace_dir) // TODO await?
- this.set(State_Key.sessions, sessions) // TODO await?
- }
-
- public get<T = string>(key: State_Key): T
- {
- return this.context.workspaceState.get(key)
- }
-
- public async set(key: State_Key, value: any)
- {
- await this.context.workspaceState.update(key, value)
- }
-}
-
-export { Workspace_State, State_Key, Setup_Data }
--- a/src/Tools/VSCode/extension/src/lsp.ts Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts Fri Mar 11 12:56:37 2022 +0100
@@ -112,26 +112,6 @@
new NotificationType<Preview_Response>("PIDE/preview_response")
-/* session theories */
-
-export interface Entries<T>
-{
- entries: T[]
-}
-
-export interface Session_Theories
-{
- session_name: string
- theories: string[]
-}
-
-export const session_theories_type =
- new NotificationType<Entries<Session_Theories>>("PIDE/session_theories")
-
-export const session_theories_request_type =
- new NotificationType<void>("PIDE/session_theories_request")
-
-
/* spell checker */
export const include_word_type =
--- a/src/Tools/VSCode/extension/src/output_view.ts Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/output_view.ts Fri Mar 11 12:56:37 2022 +0100
@@ -10,7 +10,7 @@
import { text_colors } from './decorations'
import * as vscode_lib from './vscode_lib'
import * as path from 'path'
-import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace'
+
class Output_View_Provider implements WebviewViewProvider
{
@@ -68,9 +68,7 @@
const uri = Uri.parse(link)
const line = Number(uri.fragment) || 0
const pos = new Position(line, 0)
- const uri_no_fragment = uri.with({ fragment: '' })
- const isabelle_uri = Isabelle_Workspace.get_isabelle(uri_no_fragment)
- window.showTextDocument(isabelle_uri, {
+ window.showTextDocument(uri.with({ fragment: '' }), {
preserveFocus: false,
selection: new Selection(pos, pos)
})
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/prefix_tree.ts Fri Mar 11 12:56:37 2022 +0100
@@ -0,0 +1,97 @@
+/* Author: Denis Paluca, TU Muenchen
+
+Prefix tree for symbol autocompletion.
+*/
+
+'use strict';
+
+class Tree_Node
+{
+ public key: number | string
+ public parent: Tree_Node = null
+ public end: boolean = false
+ public value: number[] | string
+ public children: Record<number | string, Tree_Node> = {}
+ constructor(key: number | string)
+ {
+ this.key = key
+ }
+
+ public get_word(): number[] | string[]
+ {
+ let output = []
+ let node: Tree_Node = this
+
+ while (node.key !== null) {
+ output.unshift(node.key)
+ node = node.parent
+ }
+
+ return output
+ }
+}
+
+class Prefix_Tree
+{
+ private root: Tree_Node
+
+ constructor()
+ {
+ this.root = new Tree_Node(null)
+ }
+
+ public insert(word: number[] | string, value: number[] | string)
+ {
+ let node = this.root
+ for (var i = 0; i < word.length; i++) {
+ if (!node.children[word[i]]) {
+ node.children[word[i]] = new Tree_Node(word[i])
+
+ node.children[word[i]].parent = node
+ }
+
+ node = node.children[word[i]]
+ node.end = false
+
+ if (i === word.length-1) {
+ node.end = true
+ node.value = value
+ }
+ }
+ }
+
+ public get_node(prefix: number[] | string): Tree_Node | undefined
+ {
+ let node = this.root
+
+ for (let i = 0; i < prefix.length; i++) {
+ if (!node.children[prefix[i]]) {
+ return
+ }
+ node = node.children[prefix[i]]
+ }
+ return node
+ }
+
+ public get_end_or_value(prefix: number[] | string): Tree_Node | undefined
+ {
+ let node = this.root
+ let resNode: Tree_Node
+ for (let i = 0; i < prefix.length; i++) {
+ if (!node.children[prefix[i]]) {
+ return resNode
+ }
+ node = node.children[prefix[i]]
+ if (node.value) {
+ resNode = node
+ }
+
+ if (node.end) {
+ return node
+ }
+ }
+ return node
+ }
+}
+
+export { Prefix_Tree, Tree_Node }
--- a/src/Tools/VSCode/extension/src/vscode_lib.ts Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/extension/src/vscode_lib.ts Fri Mar 11 12:56:37 2022 +0100
@@ -3,7 +3,6 @@
Misc library functions for VSCode.
*/
-import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace'
import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode'
@@ -11,7 +10,7 @@
export function is_file(uri: Uri): boolean
{
- return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme
+ return uri.scheme === "file"
}
export function find_file_editor(uri: Uri): TextEditor | undefined
--- a/src/Tools/VSCode/src/language_server.scala Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Fri Mar 11 12:56:37 2022 +0100
@@ -36,7 +36,6 @@
var log_file: Option[Path] = None
var logic_requirements = false
var dirs: List[Path] = Nil
- var select_dirs: List[Path] = Nil
var include_sessions: List[String] = Nil
var logic = default_logic
var modes: List[String] = Nil
@@ -51,7 +50,6 @@
-L FILE logging on FILE
-R NAME build image with requirements from other sessions
-d DIR include session directory
- -D DIR include session directory and select its sessions (without build)
-i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
-m MODE add print mode for output
@@ -64,7 +62,6 @@
"L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
"R:" -> (arg => { logic = arg; logic_requirements = true }),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(File.standard_path(arg)))),
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
@@ -78,9 +75,8 @@
val channel = new Channel(System.in, System.out, log, verbose)
val server =
new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
- select_dirs = select_dirs, include_sessions = include_sessions,
- session_ancestor = logic_ancestor, session_requirements = logic_requirements,
- modes = modes, log = log)
+ include_sessions = include_sessions, session_ancestor = logic_ancestor,
+ session_requirements = logic_requirements, modes = modes, log = log)
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
@@ -105,7 +101,6 @@
session_name: String = Language_Server.default_logic,
include_sessions: List[String] = Nil,
session_dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
session_ancestor: Option[String] = None,
session_requirements: Boolean = false,
modes: List[String] = Nil,
@@ -218,20 +213,6 @@
}
- /* session structure */
-
- def session_theories: Map[String, List[JFile]] =
- {
- val selection = Sessions.Selection.session(session_name)
- val structure =
- Sessions.load_structure(options, session_dirs, select_dirs).selection(selection)
- for {
- (name, base) <- Sessions.deps(structure).session_bases
- sources = base.session_theories.map(_.path.file)
- } yield (name, sources)
- }
-
-
/* output to client */
private val delay_output: Delay =
@@ -284,7 +265,7 @@
try {
val base_info =
Sessions.base_info(
- options, session_name, dirs = session_dirs ++ select_dirs,
+ options, session_name, dirs = session_dirs,
include_sessions = include_sessions, session_ancestor = session_ancestor,
session_requirements = session_requirements).check
@@ -485,8 +466,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.Session_Theories_Request(()) =>
- channel.write(LSP.Session_Theories(session_theories))
case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
}
}
--- a/src/Tools/VSCode/src/lsp.scala Thu Mar 10 20:16:19 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Fri Mar 11 12:56:37 2022 +0100
@@ -622,19 +622,4 @@
"label" -> label,
"content" -> content))
}
-
-
- /* Session structure */
-
- object Session_Theories_Request extends Notification0("PIDE/session_theories_request")
-
- object Session_Theories {
- def apply(session_theories: Map[String, List[JFile]]): JSON.T = {
- val entries = session_theories.map { case(session_name, theories) => JSON.Object(
- "session_name" -> session_name,
- "theories" -> theories.map(Url.print_file)
- )}
- Notification("PIDE/session_theories", JSON.Object("entries" -> entries))
- }
- }
}