more robust startup wrt. VSCode workspace (by Fabian Huch);
--- a/src/Tools/VSCode/extension/src/extension.ts Tue Feb 22 11:53:06 2022 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Tue Feb 22 12:23:21 2022 +0100
@@ -30,10 +30,10 @@
window.showErrorMessage("Missing user settings: isabelle.home")
else {
const workspace_dir = await Isabelle_FSP.register(context)
- const roots = await workspace.findFiles("{ROOT,ROOTS}")
+ const roots = workspace.workspaceFile === undefined ? await workspace.findFiles("{ROOT,ROOTS}") : []
const isabelle_tool = isabelle_home + "/bin/isabelle"
const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
- const session_args = roots.length > 0 ? ["-D", workspace_dir] : []
+ const session_args = roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : []
const server_options: ServerOptions =
library.platform_is_windows() ?
--- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts Tue Feb 22 11:53:06 2022 +0100
+++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts Tue Feb 22 12:23:21 2022 +0100
@@ -74,6 +74,7 @@
private static instance: Isabelle_FSP
private static state: Workspace_State
private static readonly draft_session = 'Draft'
+ private static readonly session_dir = 'Isabelle Sessions'
//#region public static API
@@ -82,7 +83,7 @@
public static readonly theory_extension = '.thy'
public static readonly theory_files_glob = '**/*.thy'
- public static register(context: ExtensionContext): Promise<string>
+ public static register(context: ExtensionContext): Promise<string|undefined>
{
this.instance = new Isabelle_FSP()
this.state = new Workspace_State(context)
@@ -215,26 +216,26 @@
//#region initialization
- private async setup_workspace(): Promise<string>
+ private async setup_workspace(): Promise<string|undefined>
{
const { state } = Isabelle_FSP
let { sessions, workspace_dir, symbol_entries } = state.get_setup_data()
- const main_folder_uri = Isabelle_FSP.get_dir_uri('')
- if (workspace.workspaceFolders[0].uri.toString() !== main_folder_uri.toString()) {
+ const workspace_folders = workspace.workspaceFolders || []
+ const isabelle_folder = workspace_folders.find(folder =>
+ folder.name === Isabelle_FSP.session_dir && folder.uri.scheme === Isabelle_FSP.scheme)
+
+ if (isabelle_folder === undefined) {
workspace.updateWorkspaceFolders(0, 0,
- {
- uri: main_folder_uri,
- name: 'Isabelle Sessions'
- }
- )
+ { uri: Isabelle_FSP.get_dir_uri(''), name: Isabelle_FSP.session_dir })
}
if (sessions && workspace_dir && symbol_entries) {
await Isabelle_FSP.update_symbol_encoder(symbol_entries)
await this.init_filesystem(sessions)
} else {
- workspace_dir = workspace.workspaceFolders[1].uri.fsPath
+ const default_folder = workspace_folders.find(folder => folder.uri.scheme !== Isabelle_FSP.scheme)
+ if (default_folder !== undefined) workspace_dir = default_folder.uri.fsPath
}
await state.set(State_Key.workspace_dir, workspace_dir)
@@ -423,6 +424,7 @@
private async load_theory(file_uri: Uri, isabelle_uri: Uri)
{
+ if (!this.symbol_encoder) return
const data = await workspace.fs.readFile(file_uri)
const encoded_data = this.symbol_encoder.encode(data)
await this.writeFile(isabelle_uri, encoded_data, { create: true, overwrite: true })
@@ -453,6 +455,7 @@
private async open_theory_dialogue(file_uri: Uri)
{
+ if (!this.symbol_encoder) return
const always_open = library.get_configuration<boolean>('always_open_thys')
if (!always_open) {
const answer = await window.showInformationMessage(
@@ -473,6 +476,7 @@
private async reload_theory(file_uri: Uri, isabelle_uri: Uri)
{
+ if (!this.symbol_encoder) return
const data = await workspace.fs.readFile(file_uri)
const encoded_data = this.symbol_encoder.encode(data)
await this.writeFile(isabelle_uri, encoded_data, { create: false, overwrite: true })
@@ -562,6 +566,7 @@
private async sync_original(uri: Uri, content: Uint8Array)
{
+ if (!this.symbol_encoder) return
const origin_uri = this.file_to_isabelle.get_from(uri)
const decoded_content = this.symbol_encoder.decode(content)
workspace.fs.writeFile(origin_uri, decoded_content)