# HG changeset patch # User wenzelm # Date 1646233697 -3600 # Node ID b0efc5576118ab167a329ce528ffc4bca3d185be # Parent 549e4fb76724bac647db0bdc115581240eac614b# Parent fae759dcf55fa3e53faf2f2d9c3361bb9a12dcfa merged diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/abbreviations.ts --- a/src/Tools/VSCode/extension/src/abbreviations.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/abbreviations.ts Wed Mar 02 16:08:17 2022 +0100 @@ -8,6 +8,7 @@ import { ExtensionContext, Range, TextDocumentContentChangeEvent, workspace, WorkspaceEdit } from 'vscode' import { Prefix_Tree } from './isabelle_filesystem/prefix_tree' import * as library from './library' +import * as vscode_lib from './vscode_lib' import * as symbol from './symbol' const entries: Record = {} @@ -21,7 +22,7 @@ workspace.onDidChangeTextDocument(e => { const doc = e.document - const mode = library.get_replacement_mode() + const mode = vscode_lib.get_replacement_mode() if ( mode === 'none' || doc.languageId !== 'isabelle' || diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Wed Mar 02 16:08:17 2022 +0100 @@ -6,6 +6,7 @@ TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode' import { Document_Decorations } from './protocol' import * as library from './library' +import * as vscode_lib from './vscode_lib' import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace' @@ -87,31 +88,31 @@ function background(color: string): TextEditorDecorationType { return decoration( - { light: { backgroundColor: library.get_color(color, true) }, - dark: { backgroundColor: library.get_color(color, false) } }) + { light: { backgroundColor: vscode_lib.get_color(color, true) }, + dark: { backgroundColor: vscode_lib.get_color(color, false) } }) } function text_color(color: string): TextEditorDecorationType { return decoration( - { light: { color: library.get_color(color, true) }, - dark: { color: library.get_color(color, false) } }) + { light: { color: vscode_lib.get_color(color, true) }, + dark: { color: vscode_lib.get_color(color, false) } }) } function text_overview_color(color: string): TextEditorDecorationType { return decoration( { overviewRulerLane: OverviewRulerLane.Right, - light: { overviewRulerColor: library.get_color(color, true) }, - dark: { overviewRulerColor: library.get_color(color, false) } }) + light: { overviewRulerColor: vscode_lib.get_color(color, true) }, + dark: { overviewRulerColor: vscode_lib.get_color(color, false) } }) } function bottom_border(width: string, style: string, color: string): TextEditorDecorationType { const border = `${width} none; border-bottom-style: ${style}; border-color: ` return decoration( - { light: { border: border + library.get_color(color, true) }, - dark: { border: border + library.get_color(color, false) } }) + { light: { border: border + vscode_lib.get_color(color, true) }, + dark: { border: border + vscode_lib.get_color(color, false) } }) } diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Wed Mar 02 16:08:17 2022 +0100 @@ -2,6 +2,7 @@ import * as platform from './platform' import * as library from './library' +import * as vscode_lib from './vscode_lib' import * as decorations from './decorations' import * as preview_panel from './preview_panel' import * as protocol from './protocol' @@ -30,7 +31,7 @@ const isabelle_tool = isabelle_home + "/bin/isabelle" const isabelle_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] - .concat(library.get_configuration>("args")) + .concat(vscode_lib.get_configuration>("args")) .concat(roots.length > 0 && workspace_dir !== undefined ? ["-D", workspace_dir] : []) const server_options: ServerOptions = @@ -60,7 +61,7 @@ async (progress) => { progress.report({ - message: "Waiting for Isabelle server..." + message: "Waiting for Isabelle language server..." }) await language_client.onReady() }) @@ -93,7 +94,7 @@ if (editor) { const uri = editor.document.uri const cursor = editor.selection.active - if (library.is_file(uri) && cursor) + if (vscode_lib.is_file(uri) && cursor) caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character } } if (last_caret_update !== caret_update) { @@ -117,7 +118,7 @@ caret_update.uri = Isabelle_Workspace.get_isabelle(Uri.parse(caret_update.uri)).toString() workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document => { - const editor = library.find_file_editor(document.uri) + const editor = vscode_lib.find_file_editor(document.uri) const column = editor ? editor.viewColumn : ViewColumn.One window.showTextDocument(document, column, !caret_update.focus).then(move_cursor) }) diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts --- a/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_workspace.ts Wed Mar 02 16:08:17 2022 +0100 @@ -15,6 +15,7 @@ workspace } from 'vscode'; import * as library from '../library'; +import * as vscode_lib from '../vscode_lib'; import { Session_Theories } from '../protocol'; import * as symbol from '../symbol'; import { Mapping_FSP } from './mapping_fsp'; @@ -219,7 +220,7 @@ private async open_theory_dialogue(file_uri: Uri) { - const always_open = library.get_configuration('always_open_thys') + const always_open = vscode_lib.get_configuration('always_open_thys') if (!always_open) { const answer = await window.showInformationMessage( 'Would you like to open the Isabelle theory associated with this file?', @@ -227,7 +228,7 @@ 'Always yes' ) if (answer === 'Always yes') { - library.set_configuration('always_open_thys', true) + vscode_lib.set_configuration('always_open_thys', true) } else if (answer !== 'Yes') { return } diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/library.ts --- a/src/Tools/VSCode/extension/src/library.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/library.ts Wed Mar 02 16:08:17 2022 +0100 @@ -1,9 +1,12 @@ +/* Author: Makarius + +Basic library (see Pure/library.scala). +*/ + 'use strict'; import * as platform from './platform' import * as path from 'path' -import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode' -import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace' /* regular expressions */ @@ -154,59 +157,3 @@ return result() } - - -/* files */ - -export function is_file(uri: Uri): boolean -{ - return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme -} - -export function find_file_editor(uri: Uri): TextEditor | undefined -{ - function check(editor: TextEditor): boolean - { return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath } - - if (is_file(uri)) { - if (check(window.activeTextEditor)) return window.activeTextEditor - else return window.visibleTextEditors.find(check) - } - else return undefined -} - - -/* Isabelle configuration */ - -export function get_configuration(name: string): T -{ - return workspace.getConfiguration("isabelle").get(name) -} - -export function set_configuration(name: string, configuration: T) -{ - workspace.getConfiguration("isabelle").update(name, configuration) -} - -export function get_replacement_mode() -{ - return get_configuration<"none" | "non-alphanumeric" | "all">("replacement") -} - -export function get_color(color: string, light: boolean): string -{ - const colors = get_configuration("text_color") - return colors[color + (light ? "_light" : "_dark")] -} - - -/* GUI */ - -export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn -{ - if (!editor) return ViewColumn.One - else if (!split) return editor.viewColumn - else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three) - return ViewColumn.Two - else return ViewColumn.Three -} diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/output_view.ts --- a/src/Tools/VSCode/extension/src/output_view.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/output_view.ts Wed Mar 02 16:08:17 2022 +0100 @@ -9,6 +9,7 @@ CancellationToken, window, Position, Selection, Webview} from 'vscode' import { text_colors } from './decorations' import * as library from './library' +import * as vscode_lib from './vscode_lib' import * as path from 'path' import { Isabelle_Workspace } from './isabelle_filesystem/isabelle_workspace' @@ -103,8 +104,8 @@ { let style: string = '' for (const key of text_colors) { - style += `body.vscode-light .${key} { color: ${library.get_color(key, true)} }\n` - style += `body.vscode-dark .${key} { color: ${library.get_color(key, false)} }\n` + style += `body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n` + style += `body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n` } return style diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/platform.ts --- a/src/Tools/VSCode/extension/src/platform.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/platform.ts Wed Mar 02 16:08:17 2022 +0100 @@ -1,3 +1,8 @@ +/* Author: Makarius + +System platform identification (see Pure/System/platform.scala). +*/ + 'use strict'; import * as os from 'os' diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/preview_panel.ts --- a/src/Tools/VSCode/extension/src/preview_panel.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/preview_panel.ts Wed Mar 02 16:08:17 2022 +0100 @@ -3,6 +3,7 @@ import { ExtensionContext, Uri, window, ViewColumn, WebviewPanel } from 'vscode' import { LanguageClient } from 'vscode-languageclient/node' import * as library from './library' +import * as vscode_lib from './vscode_lib' import * as protocol from './protocol' @@ -53,6 +54,6 @@ if (language_client) { language_client.sendNotification(protocol.preview_request_type, { uri: document_uri.toString(), - column: library.adjacent_editor_column(window.activeTextEditor, split) }) + column: vscode_lib.adjacent_editor_column(window.activeTextEditor, split) }) } } diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/state_panel.ts --- a/src/Tools/VSCode/extension/src/state_panel.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/state_panel.ts Wed Mar 02 16:08:17 2022 +0100 @@ -1,6 +1,7 @@ 'use strict'; import * as library from './library' +import * as vscode_lib from './vscode_lib' import * as protocol from './protocol' import {LanguageClient} from 'vscode-languageclient/node' import {ExtensionContext, Uri, ViewColumn, WebviewPanel, window} from 'vscode' @@ -11,7 +12,7 @@ function panel_column(): ViewColumn { - return library.adjacent_editor_column(window.activeTextEditor, true) + return vscode_lib.adjacent_editor_column(window.activeTextEditor, true) } class Panel diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/symbol.ts --- a/src/Tools/VSCode/extension/src/symbol.ts Wed Mar 02 15:57:04 2022 +0100 +++ b/src/Tools/VSCode/extension/src/symbol.ts Wed Mar 02 16:08:17 2022 +0100 @@ -1,3 +1,8 @@ +/* Author: Makarius + +Isabelle text symbols (see Pure/General/symbol.scala). +*/ + 'use strict'; import * as library from './library' diff -r 549e4fb76724 -r b0efc5576118 src/Tools/VSCode/extension/src/vscode_lib.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/src/vscode_lib.ts Wed Mar 02 16:08:17 2022 +0100 @@ -0,0 +1,63 @@ +/* Author: Makarius + +Misc library functions for VSCode. +*/ + +import {Isabelle_Workspace} from './isabelle_filesystem/isabelle_workspace' +import {TextEditor, Uri, ViewColumn, window, workspace} from 'vscode' + + +/* files */ + +export function is_file(uri: Uri): boolean +{ + return uri.scheme === "file" || uri.scheme === Isabelle_Workspace.scheme +} + +export function find_file_editor(uri: Uri): TextEditor | undefined +{ + function check(editor: TextEditor): boolean + { return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath } + + if (is_file(uri)) { + if (check(window.activeTextEditor)) return window.activeTextEditor + else return window.visibleTextEditors.find(check) + } + else return undefined +} + + +/* GUI */ + +export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn +{ + if (!editor) return ViewColumn.One + else if (!split) return editor.viewColumn + else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three) + return ViewColumn.Two + else return ViewColumn.Three +} + + +/* Isabelle configuration */ + +export function get_configuration(name: string): T +{ + return workspace.getConfiguration("isabelle").get(name) +} + +export function set_configuration(name: string, configuration: T) +{ + workspace.getConfiguration("isabelle").update(name, configuration) +} + +export function get_replacement_mode() +{ + return get_configuration<"none" | "non-alphanumeric" | "all">("replacement") +} + +export function get_color(color: string, light: boolean): string +{ + const colors = get_configuration("text_color") + return colors[color + (light ? "_light" : "_dark")] +}