# HG changeset patch # User wenzelm # Date 1498832205 -7200 # Node ID 8ae7c5ba1a8530a8b85923bd0b203368562df199 # Parent d4fa51e7c4ffa7dd4782417bcdf5b760f132d865 more documentation; diff -r d4fa51e7c4ff -r 8ae7c5ba1a85 src/Tools/VSCode/extension/README.md --- a/src/Tools/VSCode/extension/README.md Fri Jun 30 14:26:45 2017 +0200 +++ b/src/Tools/VSCode/extension/README.md Fri Jun 30 16:16:45 2017 +0200 @@ -1,8 +1,13 @@ # Isabelle Prover IDE support -This extension connects to the Isabelle Prover IDE infrastructure, using the -VSCode Language Server protocol. This requires a recent development version of -Isabelle from 2017, see also: +This extension connects VSCode to the Isabelle Prover IDE infrastructure. It +requires a recent development version of Isabelle from 2017 – one that happens +to fit to the extension version! + +The implementation is centered around the VSCode Language Server protocol, but +with many add-ons that to VSCode and Isabelle/PIDE. + +See also: * * @@ -10,23 +15,106 @@ ![[Isabelle/VSCode screenshot]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png) -## Prerequisites ## +## 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. -### Important User Settings ### + * Implicit formal checking of theory files, using the *cursor position* of the + active editor panel as indication for relevant spots. + + * Prover messages within the source text (errors/warnings and information + messages). + + * Semantic text decorations: colors for free/bound variables, inferred types + etc. - * On Linux and Mac OS X: `isabelle.home` points to the main Isabelle - directory (`$ISABELLE_HOME`). + * Visual indication of formal scopes and hyperlinks for formal entities. + + * Implicit proof state output via VSCode message channel ("Isabelle Output"). + + * Explicit proof state output via separate GUI panel (command + `isabelle.state`). - * On Windows: `isabelle.home` as above, but in Windows path notation with - drive-letter and backslashes. + * HTML preview via separate GUI panel (command `isabelle.preview`). + + * Rich completion information (similar to Isabelle/jEdit): 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. -### Support for Isabelle symbols ### +## Requirements + +### Isabelle Installation + + * Download a recent Isabelle development snapshot from + or the particular version + + + * 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* (e.g. version 0.20). + + + *Prettify Symbols Mode* (important for display of Isabelle symbols). + + + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus + `@{cite}` antiquotations become active for completion and hyperlinks. + + * Open the dialog *Preferences / User settings* and provide the following + entries in the second window, where local user additions are stored: + + + On all platforms: `isabelle.home` needs to point to the main Isabelle + directory (`$ISABELLE_HOME`). + + + On Windows: use drive-letter and backslashes for `isabelle.home` above. + When running from a bare repository clone, `isabelle.cygwin_home` needs to + point to a suitable Cygwin installation. + + Examples: -Isabelle symbols like `\` are rendered using the extension "Prettify -Symbols Mode", which needs to be installed separately. + + Linux: + ``` + "isabelle.home": "/home/makarius/Isabelle_01-Jul-2017" + ``` + + + Mac OS X: + ``` + "isabelle.home": "/Users/makarius/Isabelle_01-Jul-2017.app/Isabelle" + ``` + + + Windows: + ``` + "isabelle.home": "C:\\Users\\makarius\\Isabelle_01-Jul-2017" + ``` -In addition, the following user settings should be changed: + * 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 be initialized on the first opening of some Isabelle + file. It requires a few seconds to start up, with a small popup window saying + *Welcome to Isabelle*. If that fails, there might be something wrong with the + above user settings, or the Isabelle distribution does not fit to the version + of the VSCode extension from the Marketplace. + + +### Support for Isabelle symbols + +Isabelle symbols like `\` are rendered using the extension *Prettify +Symbols Mode*, which needs to be installed separately. + +In addition, the following user settings should be changed in the *Preferences / +User settings* dialog of VSCode: ``` "prettifySymbolsMode.substitutions": [ @@ -46,13 +134,16 @@ }] ``` +Actual symbol replacement tables are provided by the prover process on startup, +based on the usual `etc/symbols` specifications of the Isabelle installation. -## Further Preferences ## + +### Further Preferences * Preferred Color Theme: `Light+ (default light)` - * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some color - combinations don't work out properly. + * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some + color combinations don't work out properly. * Recommended changes to default VSCode settings: @@ -60,6 +151,30 @@ "editor.acceptSuggestionOnEnter": "off", "editor.lineNumbers": "off", "editor.renderIndentGuides": false, - "editor.rulers": [100], + "editor.rulers": [80, 100], "editor.wordBasedSuggestions": true, ``` + +## Notable Limitations of Isabelle/VSCode + + * Lack of specific support for the `IsabelleText` fonts: these need to be + manually installed on the system and configured for VSCode (cf. + `$ISABELLE_FONTS` within the Isabelle environment). + + **Note:** As the Isabelle fonts continue to evelove, installed versions need + to be updated according to each new Isabelle version. + + * Isabelle symbols are merely an optical illusion: it would be better to make + them a first-class Unicode charset as in Isabelle/jEdit. + + * Isabelle symbol abbreviations like "-->" are not accepted by VSCode. + + * Lack of formal editor perspective in VSCode: only the cursor position (with + surrounding lines of text) is used. + + * Lack of formal markup in prover messages and popups. + + * Lack of pretty-printing (line breaks) according to window and font + dimensions. + + * Lack of GUI panels for Sledgehammer, Query operations etc. diff -r d4fa51e7c4ff -r 8ae7c5ba1a85 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Fri Jun 30 14:26:45 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Fri Jun 30 16:16:45 2017 +0200 @@ -10,7 +10,7 @@ "document preparation" ], "icon": "isabelle.png", - "version": "0.19.0", + "version": "0.20.0", "publisher": "makarius", "license": "MIT", "repository": {