src/Tools/VSCode/extension/README.md
author wenzelm
Tue, 23 Apr 2024 15:57:03 +0200
changeset 80145 0eff7d113549
parent 75347 b75fefe1ddb5
permissions -rw-r--r--
update Windows build host;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     1
# Isabelle/VSCode Prover IDE
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     2
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     3
## General notes
64757
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
     4
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     5
This is the Isabelle/VSCode extension to connect VSCodium to
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     6
Isabelle/PIDE. The application is invoked via `isabelle vscode` on the
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     7
command-line. It takes care about configuring the extension and user
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
     8
settings.
66236
8ae7c5ba1a85 more documentation;
wenzelm
parents: 66230
diff changeset
     9
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    10
The implementation is centered around the VSCode Language Server
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    11
Protocol (LSP), but there are many add-ons that are specific to
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    12
Isabelle/PIDE. Moreover, there are important patches to the VSCodium
75347
b75fefe1ddb5 tuned text, without update of component for now;
wenzelm
parents: 75338
diff changeset
    13
code-base itself, e.g. to support the UTF-8-Isabelle encoding for
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    14
mathematical symbols and to incorporate the corresponding Isabelle
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    15
fonts. It is unlikely that this extension will with regular VSCode nor
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    16
with any other LSP-based editor.
64757
7e3924224769 updated package;
wenzelm
parents: 64605
diff changeset
    17
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    18
Isabelle/VSCode works best when opening an Isabelle project directory
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    19
as a "workspace", with explorer access to the sources.  Afterwards it
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    20
is possible to edit `.thy` and `.ML` files with semantic checking by
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    21
the prover in the background, similar to Isabelle/jEdit. There is also
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    22
support for other file formats, e.g. `bib` for bibliographic
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    23
databases, which may be combined with a regular VSCode extension for
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    24
LaTeX/BibTeX.
66227
wenzelm
parents: 66224
diff changeset
    25
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    26
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    27
## Known limitations of Isabelle/VSCode
66236
8ae7c5ba1a85 more documentation;
wenzelm
parents: 66230
diff changeset
    28
66237
wenzelm
parents: 66236
diff changeset
    29
  * Lack of formal editor perspective in VSCode: only the cursor position is
wenzelm
parents: 66236
diff changeset
    30
  used (with some surrounding lines of text).
66236
8ae7c5ba1a85 more documentation;
wenzelm
parents: 66230
diff changeset
    31
66237
wenzelm
parents: 66236
diff changeset
    32
  * Lack of pretty-printing (logical line breaks) according to window and font
66236
8ae7c5ba1a85 more documentation;
wenzelm
parents: 66230
diff changeset
    33
  dimensions.
8ae7c5ba1a85 more documentation;
wenzelm
parents: 66230
diff changeset
    34
66240
1a04946c41d6 tuned documentation;
wenzelm
parents: 66237
diff changeset
    35
  * Big theory files may cause problems to the VSCode rendering engine, since
1a04946c41d6 tuned documentation;
wenzelm
parents: 66237
diff changeset
    36
  messages and text decorations are applied to the text as a whole (cf. the
1a04946c41d6 tuned documentation;
wenzelm
parents: 66237
diff changeset
    37
  minimap view).
75338
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    38
73034d385688 updated vscode_extension;
wenzelm
parents: 75158
diff changeset
    39
  * Overall lack of features and refinements compared to Isabelle/jEdit.