# HG changeset patch # User wenzelm # Date 1648211126 -3600 # Node ID 73034d38568846e28ceb97973a7cdd47f7f26c1a # Parent 28d2cb99b37f2dee06c12c5adbce2126ef069720 updated vscode_extension; diff -r 28d2cb99b37f -r 73034d385688 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Mar 25 10:45:47 2022 +0100 +++ b/Admin/components/components.sha1 Fri Mar 25 13:25:26 2022 +0100 @@ -447,6 +447,7 @@ b576fd5d89767c1067541d4839fb749c6a68d22c verit-2021.06.1-rmx.tar.gz 19c6e5677b0a26cbc5805da79d00d06a66b7a671 verit-2021.06.2-rmx.tar.gz c4666a6d8080b5e376b50471fd2d9edeb1f9c988 vscode_extension-20220324.tar.gz +86c952d739d1eb868be88898982d4870a3d8c2dc vscode_extension-20220325.tar.gz 67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz diff -r 28d2cb99b37f -r 73034d385688 Admin/components/main --- a/Admin/components/main Fri Mar 25 10:45:47 2022 +0100 +++ b/Admin/components/main Fri Mar 25 13:25:26 2022 +0100 @@ -29,7 +29,7 @@ stack-2.7.3 vampire-4.6 verit-2021.06.2-rmx -vscode_extension-20220324 +vscode_extension-20220325 vscodium-1.65.2 xz-java-1.9 z3-4.4.0_4.4.1 diff -r 28d2cb99b37f -r 73034d385688 src/Tools/VSCode/extension/README.md --- a/src/Tools/VSCode/extension/README.md Fri Mar 25 10:45:47 2022 +0100 +++ b/src/Tools/VSCode/extension/README.md Fri Mar 25 13:25:26 2022 +0100 @@ -1,115 +1,39 @@ -# Isabelle Prover IDE support +# Isabelle/VSCode Prover IDE + +## General notes -This extension connects VSCode to the Isabelle Prover IDE infrastructure: it -requires a suitable repository version of Isabelle. - -The implementation is centered around the VSCode Language Server protocol, but -with many add-ons that are specific to VSCode and Isabelle/PIDE. +This is the Isabelle/VSCode extension to connect VSCodium to +Isabelle/PIDE. The application is invoked via `isabelle vscode` on the +command-line. It takes care about configuring the extension and user +settings. -See also: - - * - * +The implementation is centered around the VSCode Language Server +Protocol (LSP), but there are many add-ons that are specific to +Isabelle/PIDE. Moreover, there are important patches to the VSCodium +code-base itself, e.g. to support the UTF8-Isabelle encoding for +mathematical symbols and to incorporate the corresponding Isabelle +fonts. It is unlikely that this extension will with regular VSCode nor +with any other LSP-based editor. - -## Screenshot - -![[Isabelle/VSCode]](https://isabelle.in.tum.de/repos/isabelle/raw-file/b565a39627bb/src/Tools/VSCode/extension/isabelle_vscode.png) +Isabelle/VSCode works best when opening an Isabelle project directory +as a "workspace", with explorer access to the sources. Afterwards it +is possible to edit `.thy` and `.ML` files with semantic checking by +the prover in the background, similar to Isabelle/jEdit. There is also +support for other file formats, e.g. `bib` for bibliographic +databases, which may be combined with a regular VSCode extension for +LaTeX/BibTeX. -## Notable Features - - * Static syntax tables for Isabelle `.thy` and `.ML` files. - - * Implicit dependency management of sources, subject to changes of theory - files within the editor, as well as external file-system events. - - * Implicit formal checking of theory files, using the *cursor position* of the - active editor panel as indication for relevant spots. - - * Text overview lane with formal status of prover commands (unprocessed, - running, error, warning). - - * Prover messages within the source text (errors/warnings and information - messages). - - * Semantic text decorations: colors for free/bound variables, inferred types - etc. - - * Visual indication of formal scopes and hyperlinks for formal entities. - - * Implicit proof state output via the VSCode message channel "Isabelle - Output". - - * Explicit proof state output via separate GUI panel (command - `isabelle.state`). - - * HTML preview via separate GUI panel (command `isabelle.preview`). - - * Rich completion information: Isabelle symbols (e.g. `\forall` or - `\`), outer syntax keywords, formal entities, file-system paths, - BibTeX entries etc. - - * Spell-checking of informal texts, including dictionary operations: via the - regular completion dialog. - - -## Requirements - -### Isabelle/VSCode Installation - - * Download a recent Isabelle development snapshot from - - - * Unpack and run the main Isabelle/jEdit application as usual, to ensure that - the logic image is built properly and Isabelle works as expected. - - * Download and install VSCode from - - * Open the VSCode *Extensions* view and install the following: - - + *Isabelle* (needs to fit to the underlying Isabelle release). - - + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus - `@{cite}` antiquotations become active for completion and hyperlinks. - - * Restart the VSCode application to ensure that all extensions are properly - initialized and user settings are updated. Afterwards VSCode should know about - `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules). - - The Isabelle extension is initialized when the first Isabelle file is opened. - It requires a few seconds to start up: a small popup window eventually says - *"Welcome to Isabelle ..."*. - - -### Further Preferences - - * Preferred Color Theme: `Light+ (default light)` - - * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some - color combinations don't work out properly. - - * Recommended changes to default VSCode settings: - - ``` - "editor.acceptSuggestionOnEnter": "off", - "editor.wordBasedSuggestions": true, - ``` - -## Known Limitations of Isabelle/VSCode - - * Isabelle symbol abbreviations like "-->" are not accepted by VSCode. +## Known limitations of Isabelle/VSCode * Lack of formal editor perspective in VSCode: only the cursor position is used (with some surrounding lines of text). - * Lack of formal markup in prover messages and popups. - * Lack of pretty-printing (logical line breaks) according to window and font dimensions. - * Lack of GUI panels for Sledgehammer, Query operations etc. - * Big theory files may cause problems to the VSCode rendering engine, since messages and text decorations are applied to the text as a whole (cf. the minimap view). + + * Overall lack of features and refinements compared to Isabelle/jEdit.