src/Tools/VSCode/extension/README.md
changeset 66237 93eac3bdf3f9
parent 66236 8ae7c5ba1a85
child 66240 1a04946c41d6
equal deleted inserted replaced
66236:8ae7c5ba1a85 66237:93eac3bdf3f9
     3 This extension connects VSCode to the Isabelle Prover IDE infrastructure. It
     3 This extension connects VSCode to the Isabelle Prover IDE infrastructure. It
     4 requires a recent development version of Isabelle from 2017 – one that happens
     4 requires a recent development version of Isabelle from 2017 – one that happens
     5 to fit to the extension version!
     5 to fit to the extension version!
     6 
     6 
     7 The implementation is centered around the VSCode Language Server protocol, but
     7 The implementation is centered around the VSCode Language Server protocol, but
     8 with many add-ons that to VSCode and Isabelle/PIDE.
     8 with many add-ons that are specific to VSCode and Isabelle/PIDE.
     9 
     9 
    10 See also:
    10 See also:
    11 
    11 
    12   * <http://isabelle.in.tum.de/devel/release_snapshot>
    12   * <http://isabelle.in.tum.de/devel/release_snapshot>
    13   * <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
    13   * <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
       
    14   * <https://github.com/Microsoft/language-server-protocol>
    14 
    15 
    15 ![[Isabelle/VSCode screenshot]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png)
    16 
       
    17 ## Screenshot
       
    18 
       
    19 ![[Isabelle/VSCode]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png)
    16 
    20 
    17 
    21 
    18 ## Notable Features
    22 ## Notable Features
    19 
    23 
    20   * Static syntax tables for Isabelle `.thy` and `.ML` files.
    24   * Static syntax tables for Isabelle `.thy` and `.ML` files.
    31   * Semantic text decorations: colors for free/bound variables, inferred types
    35   * Semantic text decorations: colors for free/bound variables, inferred types
    32   etc.
    36   etc.
    33 
    37 
    34   * Visual indication of formal scopes and hyperlinks for formal entities.
    38   * Visual indication of formal scopes and hyperlinks for formal entities.
    35 
    39 
    36   * Implicit proof state output via VSCode message channel ("Isabelle Output").
    40   * Implicit proof state output via the VSCode message channel "Isabelle
       
    41   Output".
    37 
    42 
    38   * Explicit proof state output via separate GUI panel (command
    43   * Explicit proof state output via separate GUI panel (command
    39   `isabelle.state`).
    44   `isabelle.state`).
    40 
    45 
    41   * HTML preview via separate GUI panel (command `isabelle.preview`).
    46   * HTML preview via separate GUI panel (command `isabelle.preview`).
    42 
    47 
    43   * Rich completion information (similar to Isabelle/jEdit): Isabelle symbols
    48   * Rich completion information: Isabelle symbols (e.g. `\forall` or
    44   (e.g. `\forall` or `\<forall>`), outer syntax keywords, formal entities,
    49   `\<forall>`), outer syntax keywords, formal entities, file-system paths,
    45   file-system paths, BibTeX entries etc.
    50   BibTeX entries etc.
    46 
    51 
    47   * Spell-checking of informal texts, including dictionary operations: via the
    52   * Spell-checking of informal texts, including dictionary operations: via the
    48   regular completion dialog.
    53   regular completion dialog.
    49 
    54 
    50 
    55 
    75 
    80 
    76       + On all platforms: `isabelle.home` needs to point to the main Isabelle
    81       + On all platforms: `isabelle.home` needs to point to the main Isabelle
    77       directory (`$ISABELLE_HOME`).
    82       directory (`$ISABELLE_HOME`).
    78 
    83 
    79       + On Windows: use drive-letter and backslashes for `isabelle.home` above.
    84       + On Windows: use drive-letter and backslashes for `isabelle.home` above.
    80       When running from a bare repository clone, `isabelle.cygwin_home` needs to
    85       When running from a bare repository clone (not a development snapshot),
    81       point to a suitable Cygwin installation.
    86       `isabelle.cygwin_home` needs to point to a suitable Cygwin installation.
    82 
    87 
    83     Examples:
    88     Examples:
    84 
    89 
    85       + Linux:
    90       + Linux:
    86         ```
    91         ```
    99 
   104 
   100   * Restart the VSCode application to ensure that all extensions are properly
   105   * Restart the VSCode application to ensure that all extensions are properly
   101   initialized and user settings are updated. Afterwards VSCode should know about
   106   initialized and user settings are updated. Afterwards VSCode should know about
   102   `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
   107   `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
   103 
   108 
   104   The Isabelle extension is be initialized on the first opening of some Isabelle
   109   The Isabelle extension is initialized when the first Isabelle is opened. It
   105   file. It requires a few seconds to start up, with a small popup window saying
   110   requires a few seconds to start up: a small popup window says *Welcome to
   106   *Welcome to Isabelle*. If that fails, there might be something wrong with the
   111   Isabelle*. If that fails, there might be something wrong with `isabelle.home`
   107   above user settings, or the Isabelle distribution does not fit to the version
   112   from above, or the Isabelle distribution does not fit to the version of the
   108   of the VSCode extension from the Marketplace.
   113   VSCode extension from the Marketplace.
   109 
   114 
   110 
   115 
   111 ### Support for Isabelle symbols
   116 ### Support for Isabelle symbols
   112 
   117 
   113 Isabelle symbols like `\<forall>` are rendered using the extension *Prettify
   118 Isabelle symbols like `\<forall>` are rendered using the extension *Prettify
   153     "editor.renderIndentGuides": false,
   158     "editor.renderIndentGuides": false,
   154     "editor.rulers": [80, 100],
   159     "editor.rulers": [80, 100],
   155     "editor.wordBasedSuggestions": true,
   160     "editor.wordBasedSuggestions": true,
   156     ```
   161     ```
   157 
   162 
   158 ## Notable Limitations of Isabelle/VSCode
   163 ## Known Limitations of Isabelle/VSCode
   159 
   164 
   160   * Lack of specific support for the `IsabelleText` fonts: these need to be
   165   * Lack of specific support for the `IsabelleText` fonts: these need to be
   161   manually installed on the system and configured for VSCode (cf.
   166   manually installed on the system and configured for VSCode (see also
   162   `$ISABELLE_FONTS` within the Isabelle environment).
   167   `$ISABELLE_FONTS` within the Isabelle environment).
   163 
   168 
   164     **Note:** As the Isabelle fonts continue to evelove, installed versions need
   169     **Note:** As the Isabelle fonts continue to evolve, installed versions need
   165     to be updated according to each new Isabelle version.
   170     to be updated according to each new Isabelle version.
   166 
   171 
   167   * Isabelle symbols are merely an optical illusion: it would be better to make
   172   * Isabelle symbols are merely an optical illusion: it would be better to make
   168     them a first-class Unicode charset as in Isabelle/jEdit.
   173     them a first-class Unicode charset as in Isabelle/jEdit.
   169 
   174 
   170   * Isabelle symbol abbreviations like "-->" are not accepted by VSCode.
   175   * Isabelle symbol abbreviations like "-->" are not accepted by VSCode.
   171 
   176 
   172   * Lack of formal editor perspective in VSCode: only the cursor position (with
   177   * Lack of formal editor perspective in VSCode: only the cursor position is
   173   surrounding lines of text) is used.
   178   used (with some surrounding lines of text).
   174 
   179 
   175   * Lack of formal markup in prover messages and popups.
   180   * Lack of formal markup in prover messages and popups.
   176 
   181 
   177   * Lack of pretty-printing (line breaks) according to window and font
   182   * Lack of pretty-printing (logical line breaks) according to window and font
   178   dimensions.
   183   dimensions.
   179 
   184 
   180   * Lack of GUI panels for Sledgehammer, Query operations etc.
   185   * Lack of GUI panels for Sledgehammer, Query operations etc.