# HG changeset patch
# User wenzelm
# Date 1646999797 -3600
# Node ID ec62c54015225b11350861d5ba61af54865d7ba9
# Parent  ed83c58c612ad177f43d9ae533a9475996a32aaa
discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
discontinued special treatment of workspace_dir as session directory;

diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/package.json
--- 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": {
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/abbreviations.ts
--- 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'
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/decorations.ts
--- 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)
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/extension.ts
--- 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(() =>
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts
--- 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
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/isabelle_filesystem/mapping_fsp.ts
--- 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
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts
--- 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 }
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts
--- 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)
-  }
-}
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts
--- 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
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts
--- 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 }
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/lsp.ts
--- 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 =
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/output_view.ts
--- 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)
   })
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/prefix_tree.ts
--- /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 }
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/extension/src/vscode_lib.ts
--- 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
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/src/language_server.scala
--- 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")
         }
       }
diff -r ed83c58c612a -r ec62c5401522 src/Tools/VSCode/src/lsp.scala
--- 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))
-    }
-  }
 }