src/Tools/VSCode/extension/README.md
author wenzelm
Thu, 29 Jun 2017 21:43:55 +0200
changeset 66223 a6fdb22b0ce2
parent 66221 e6b7edd12f05
child 66224 9fe05edaa351
permissions -rw-r--r--
clarified;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64757
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     1
# Isabelle Prover IDE support
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     2
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     3
This extension connects to the Isabelle Prover IDE infrastructure, using the
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     4
VSCode Language Server protocol. This requires a recent development version of
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     5
Isabelle from 2017, see also:
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     6
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
     7
  * <http://isabelle.in.tum.de/devel/release_snapshot>
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
     8
  * <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
64757
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     9
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    10
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    11
## Prerequisites ##
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    12
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    13
### Important User Settings ###
64757
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
    14
64948
wenzelm
parents: 64873
diff changeset
    15
  * On Linux and Mac OS X: `isabelle.home` points to the main Isabelle
wenzelm
parents: 64873
diff changeset
    16
    directory (`$ISABELLE_HOME`).
wenzelm
parents: 64873
diff changeset
    17
wenzelm
parents: 64873
diff changeset
    18
  * On Windows: `isabelle.home` as above, but in Windows path notation with
wenzelm
parents: 64873
diff changeset
    19
    drive-letter and backslashes.
wenzelm
parents: 64873
diff changeset
    20
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    21
### Support for Isabelle symbols ###
64873
ee5aaf7bce0d more documentation;
wenzelm
parents: 64757
diff changeset
    22
66070
65a68dcd95c3 dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents: 65172
diff changeset
    23
Isabelle symbols like `\<forall>` are rendered using the extension "Prettify
65a68dcd95c3 dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents: 65172
diff changeset
    24
Symbols Mode", which needs to be installed separately.
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    25
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    26
In addition, the following user settings should be changed:
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    27
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    28
```
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    29
"prettifySymbolsMode.substitutions": [
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    30
  {
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    31
    "language": "isabelle",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    32
    "revealOn": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    33
    "adjustCursorMovement": true,
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    34
    "prettyCursor": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    35
    "substitutions": []
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    36
  },
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    37
  {
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    38
    "language": "isabelle-ml",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    39
    "revealOn": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    40
    "adjustCursorMovement": true,
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    41
    "prettyCursor": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    42
    "substitutions": []
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    43
  }]
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    44
```
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    45
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    46
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    47
## Further Preferences ##
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    48
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    49
  * Preferred Color Theme: `Light+ (default light)`
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    50
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    51
  * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some color
66221
wenzelm
parents: 66218
diff changeset
    52
    combinations don't work out properly.
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    53
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    54
  * Recommended changes to default VSCode settings:
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    55
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    56
    ```
66223
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    57
    "editor.acceptSuggestionOnEnter": "off",
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    58
    "editor.lineNumbers": "off",
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    59
    "editor.renderIndentGuides": false,
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    60
    "editor.rulers": [100],
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    61
    "editor.wordBasedSuggestions": true,
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    62
    ```