|
64757
|
1 |
# Isabelle Prover IDE support
|
|
|
2 |
|
|
|
3 |
This extension connects to the Isabelle Prover IDE infrastructure, using the
|
|
|
4 |
VSCode Language Server protocol. This requires a recent development version of
|
|
|
5 |
Isabelle from 2017, see also:
|
|
64605
|
6 |
|
|
64757
|
7 |
* http://isabelle.in.tum.de/devel
|
|
|
8 |
* http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode
|
|
|
9 |
|
|
64605
|
10 |
|
|
64757
|
11 |
## Important User Settings ##
|
|
|
12 |
|
|
64948
|
13 |
* On Linux and Mac OS X: `isabelle.home` points to the main Isabelle
|
|
|
14 |
directory (`$ISABELLE_HOME`).
|
|
|
15 |
|
|
|
16 |
* On Windows: `isabelle.home` as above, but in Windows path notation with
|
|
|
17 |
drive-letter and backslashes.
|
|
|
18 |
|
|
|
19 |
Moreover, `isabelle.cygwin_root` needs to point to a suitable Cygwin
|
|
|
20 |
installation, e.g. `$ISABELLE_HOME\contrib\cygwin` for a regular Isabelle
|
|
|
21 |
application bundle, or `C:\cygwin` for a stand-alone installation used
|
|
|
22 |
with Isabelle repository snapshot.
|
|
64873
|
23 |
|
|
|
24 |
|
|
|
25 |
## Isabelle symbols ##
|
|
|
26 |
|
|
|
27 |
Isabelle symbols like `\<forall>` may be rendered using the extension Prettify
|
|
|
28 |
Symbols Mode. It needs to be configured manually as follows:
|
|
|
29 |
|
|
64948
|
30 |
$ISABELLE_HOME/src/Tools/VSCode/extension/isabelle-symbols.json contains a
|
|
64873
|
31 |
configuration (generated via `isabelle vscode_symbols`). Its content needs to
|
|
|
32 |
be copied carefully into the regular VSCode User Preferences.
|