--- 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:
* <http://isabelle.in.tum.de/devel/release_snapshot>
* <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
@@ -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 `\<forall>`), 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
+ <http://isabelle.in.tum.de/devel/release_snapshot> or the particular version
+ <http://www4.in.tum.de/~wenzelm/Isabelle_01-Jul-2017>
+
+ * 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 <https://code.visualstudio.com>
+
+ * 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 `\<forall>` 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 `\<forall>` 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.
--- 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": {