tuned;
authorwenzelm
Fri Jun 30 16:28:06 2017 +0200 (23 months ago)
changeset 6623793eac3bdf3f9
parent 66236 8ae7c5ba1a85
child 66238 88b8ef0b17fd
tuned;
src/Tools/VSCode/extension/README.md
src/Tools/VSCode/extension/package.json
     1.1 --- a/src/Tools/VSCode/extension/README.md	Fri Jun 30 16:16:45 2017 +0200
     1.2 +++ b/src/Tools/VSCode/extension/README.md	Fri Jun 30 16:28:06 2017 +0200
     1.3 @@ -5,14 +5,18 @@
     1.4  to fit to the extension version!
     1.5  
     1.6  The implementation is centered around the VSCode Language Server protocol, but
     1.7 -with many add-ons that to VSCode and Isabelle/PIDE.
     1.8 +with many add-ons that are specific to VSCode and Isabelle/PIDE.
     1.9  
    1.10  See also:
    1.11  
    1.12    * <http://isabelle.in.tum.de/devel/release_snapshot>
    1.13    * <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
    1.14 +  * <https://github.com/Microsoft/language-server-protocol>
    1.15  
    1.16 -![[Isabelle/VSCode screenshot]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png)
    1.17 +
    1.18 +## Screenshot
    1.19 +
    1.20 +![[Isabelle/VSCode]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png)
    1.21  
    1.22  
    1.23  ## Notable Features
    1.24 @@ -33,16 +37,17 @@
    1.25  
    1.26    * Visual indication of formal scopes and hyperlinks for formal entities.
    1.27  
    1.28 -  * Implicit proof state output via VSCode message channel ("Isabelle Output").
    1.29 +  * Implicit proof state output via the VSCode message channel "Isabelle
    1.30 +  Output".
    1.31  
    1.32    * Explicit proof state output via separate GUI panel (command
    1.33    `isabelle.state`).
    1.34  
    1.35    * HTML preview via separate GUI panel (command `isabelle.preview`).
    1.36  
    1.37 -  * Rich completion information (similar to Isabelle/jEdit): Isabelle symbols
    1.38 -  (e.g. `\forall` or `\<forall>`), outer syntax keywords, formal entities,
    1.39 -  file-system paths, BibTeX entries etc.
    1.40 +  * Rich completion information: Isabelle symbols (e.g. `\forall` or
    1.41 +  `\<forall>`), outer syntax keywords, formal entities, file-system paths,
    1.42 +  BibTeX entries etc.
    1.43  
    1.44    * Spell-checking of informal texts, including dictionary operations: via the
    1.45    regular completion dialog.
    1.46 @@ -77,8 +82,8 @@
    1.47        directory (`$ISABELLE_HOME`).
    1.48  
    1.49        + On Windows: use drive-letter and backslashes for `isabelle.home` above.
    1.50 -      When running from a bare repository clone, `isabelle.cygwin_home` needs to
    1.51 -      point to a suitable Cygwin installation.
    1.52 +      When running from a bare repository clone (not a development snapshot),
    1.53 +      `isabelle.cygwin_home` needs to point to a suitable Cygwin installation.
    1.54  
    1.55      Examples:
    1.56  
    1.57 @@ -101,11 +106,11 @@
    1.58    initialized and user settings are updated. Afterwards VSCode should know about
    1.59    `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
    1.60  
    1.61 -  The Isabelle extension is be initialized on the first opening of some Isabelle
    1.62 -  file. It requires a few seconds to start up, with a small popup window saying
    1.63 -  *Welcome to Isabelle*. If that fails, there might be something wrong with the
    1.64 -  above user settings, or the Isabelle distribution does not fit to the version
    1.65 -  of the VSCode extension from the Marketplace.
    1.66 +  The Isabelle extension is initialized when the first Isabelle is opened. It
    1.67 +  requires a few seconds to start up: a small popup window says *Welcome to
    1.68 +  Isabelle*. If that fails, there might be something wrong with `isabelle.home`
    1.69 +  from above, or the Isabelle distribution does not fit to the version of the
    1.70 +  VSCode extension from the Marketplace.
    1.71  
    1.72  
    1.73  ### Support for Isabelle symbols
    1.74 @@ -155,13 +160,13 @@
    1.75      "editor.wordBasedSuggestions": true,
    1.76      ```
    1.77  
    1.78 -## Notable Limitations of Isabelle/VSCode
    1.79 +## Known Limitations of Isabelle/VSCode
    1.80  
    1.81    * Lack of specific support for the `IsabelleText` fonts: these need to be
    1.82 -  manually installed on the system and configured for VSCode (cf.
    1.83 +  manually installed on the system and configured for VSCode (see also
    1.84    `$ISABELLE_FONTS` within the Isabelle environment).
    1.85  
    1.86 -    **Note:** As the Isabelle fonts continue to evelove, installed versions need
    1.87 +    **Note:** As the Isabelle fonts continue to evolve, installed versions need
    1.88      to be updated according to each new Isabelle version.
    1.89  
    1.90    * Isabelle symbols are merely an optical illusion: it would be better to make
    1.91 @@ -169,12 +174,12 @@
    1.92  
    1.93    * Isabelle symbol abbreviations like "-->" are not accepted by VSCode.
    1.94  
    1.95 -  * Lack of formal editor perspective in VSCode: only the cursor position (with
    1.96 -  surrounding lines of text) is used.
    1.97 +  * Lack of formal editor perspective in VSCode: only the cursor position is
    1.98 +  used (with some surrounding lines of text).
    1.99  
   1.100    * Lack of formal markup in prover messages and popups.
   1.101  
   1.102 -  * Lack of pretty-printing (line breaks) according to window and font
   1.103 +  * Lack of pretty-printing (logical line breaks) according to window and font
   1.104    dimensions.
   1.105  
   1.106    * Lack of GUI panels for Sledgehammer, Query operations etc.
     2.1 --- a/src/Tools/VSCode/extension/package.json	Fri Jun 30 16:16:45 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Jun 30 16:28:06 2017 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4          "document preparation"
     2.5      ],
     2.6      "icon": "isabelle.png",
     2.7 -    "version": "0.20.0",
     2.8 +    "version": "0.21.0",
     2.9      "publisher": "makarius",
    2.10      "license": "MIT",
    2.11      "repository": {