src/Tools/VSCode/extension/README.md

   * <https://github.com/Microsoft/language-server-protocol>
 
 
 ## Screenshot
 
-![[Isabelle/VSCode]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png)
+![[Isabelle/VSCode]](http://isabelle.in.tum.de/repos/isabelle/raw-file/b565a39627bb/src/Tools/VSCode/extension/isabelle_vscode.png)
 
 
 ## 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

   regular completion dialog.
 
 
 ## Requirements
 
-### Isabelle Installation
+### Isabelle/VSCode 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>
 

 
   * Download and install VSCode from <https://code.visualstudio.com>
 
   * Open the VSCode *Extensions* view and install the following:
 
-      + *Isabelle* (e.g. version 0.20).
+      + *Isabelle* (e.g. version 0.22).
 
       + *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.

 
   * 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 is opened. It
-  requires a few seconds to start up: a small popup window says *Welcome to
-  Isabelle*. If that fails, there might be something wrong with `isabelle.home`
-  from above, or the Isabelle distribution does not fit to the version of the
-  VSCode extension from the Marketplace.
+  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 ..."*. If that fails, there might be something wrong
+  with `isabelle.home` from above, 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

 
   * 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).