src/Tools/VSCode/extension/README.md
author wenzelm
Thu, 29 Jun 2017 23:06:20 +0200
changeset 66229 d3b6e5e47015
parent 66227 7470985f3fb6
child 66230 ae814012b95f
permissions -rw-r--r--
updated package;
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
66227
wenzelm
parents: 66224
diff changeset
    10
![[Isabelle/VSCode screenshot]](isabelle_vscode.png)
wenzelm
parents: 66224
diff changeset
    11
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    13
## Prerequisites ##
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    14
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    15
### Important User Settings ###
64757
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
    16
64948
wenzelm
parents: 64873
diff changeset
    17
  * On Linux and Mac OS X: `isabelle.home` points to the main Isabelle
wenzelm
parents: 64873
diff changeset
    18
    directory (`$ISABELLE_HOME`).
wenzelm
parents: 64873
diff changeset
    19
wenzelm
parents: 64873
diff changeset
    20
  * On Windows: `isabelle.home` as above, but in Windows path notation with
wenzelm
parents: 64873
diff changeset
    21
    drive-letter and backslashes.
wenzelm
parents: 64873
diff changeset
    22
66227
wenzelm
parents: 66224
diff changeset
    23
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    24
### Support for Isabelle symbols ###
64873
ee5aaf7bce0d more documentation;
wenzelm
parents: 64757
diff changeset
    25
66070
65a68dcd95c3 dynamic configuration of prettify-symbols-mode, similar to VSCoq;
wenzelm
parents: 65172
diff changeset
    26
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
    27
Symbols Mode", which needs to be installed separately.
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    28
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    29
In addition, the following user settings should be changed:
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    30
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    31
```
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    32
"prettifySymbolsMode.substitutions": [
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    33
  {
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    34
    "language": "isabelle",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    35
    "revealOn": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    36
    "adjustCursorMovement": true,
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    37
    "prettyCursor": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    38
    "substitutions": []
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    39
  },
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    40
  {
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    41
    "language": "isabelle-ml",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    42
    "revealOn": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    43
    "adjustCursorMovement": true,
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    44
    "prettyCursor": "none",
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    45
    "substitutions": []
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    46
  }]
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    47
```
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    48
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    49
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    50
## Further Preferences ##
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    51
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    52
  * Preferred Color Theme: `Light+ (default light)`
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    53
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    54
  * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some color
66221
wenzelm
parents: 66218
diff changeset
    55
    combinations don't work out properly.
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    56
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    57
  * Recommended changes to default VSCode settings:
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    58
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    59
    ```
66223
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    60
    "editor.acceptSuggestionOnEnter": "off",
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    61
    "editor.lineNumbers": "off",
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    62
    "editor.renderIndentGuides": false,
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    63
    "editor.rulers": [100],
a6fdb22b0ce2 clarified;
wenzelm
parents: 66221
diff changeset
    64
    "editor.wordBasedSuggestions": true,
66218
a30bf1c755c1 more documentation;
wenzelm
parents: 66070
diff changeset
    65
    ```