src/Tools/VSCode/extension/README.md
changeset 68870 53a75627aab7
parent 68546 34d732a83767
child 69343 395c4fb15ea2
equal deleted inserted replaced
68869:3739acbc2178 68870:53a75627aab7
     1 # Isabelle Prover IDE support
     1 # Isabelle Prover IDE support
     2 
     2 
     3 This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
     3 This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
     4 requires Isabelle2018.
     4 requires a repository version of Isabelle.
     5 
     5 
     6 The implementation is centered around the VSCode Language Server protocol, but
     6 The implementation is centered around the VSCode Language Server protocol, but
     7 with many add-ons that are specific to VSCode and Isabelle/PIDE.
     7 with many add-ons that are specific to VSCode and Isabelle/PIDE.
     8 
     8 
     9 See also:
     9 See also:
    10 
    10 
    11   * <https://isabelle.in.tum.de/website-Isabelle2018>
    11   * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
    12   * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Tools/VSCode>
       
    13   * <https://github.com/Microsoft/language-server-protocol>
    12   * <https://github.com/Microsoft/language-server-protocol>
    14 
    13 
    15 
    14 
    16 ## Screenshot
    15 ## Screenshot
    17 
    16 
    57 
    56 
    58 ## Requirements
    57 ## Requirements
    59 
    58 
    60 ### Isabelle/VSCode Installation
    59 ### Isabelle/VSCode Installation
    61 
    60 
    62   * Download Isabelle2018 from <https://isabelle.in.tum.de/website-Isabelle2018>
    61   * Download a recent Isabelle development snapshot from <http://isabelle.in.tum.de/devel/release_snapshot>
    63     or any of its mirror sites.
       
    64 
    62 
    65   * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
    63   * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
    66   the logic image is built properly and Isabelle works as expected.
    64   the logic image is built properly and Isabelle works as expected.
    67 
    65 
    68   * Download and install VSCode from <https://code.visualstudio.com>
    66   * Download and install VSCode from <https://code.visualstudio.com>
    69 
    67 
    70   * Open the VSCode *Extensions* view and install the following:
    68   * Open the VSCode *Extensions* view and install the following:
    71 
    69 
    72       + *Isabelle2018* (needs to fit to the underlying Isabelle release).
    70       + *Isabelle*.
    73 
    71 
    74       + *Prettify Symbols Mode* (important for display of Isabelle symbols).
    72       + *Prettify Symbols Mode* (important for display of Isabelle symbols).
    75 
    73 
    76       + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus
    74       + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus
    77         `@{cite}` antiquotations become active for completion and hyperlinks.
    75         `@{cite}` antiquotations become active for completion and hyperlinks.
    88 
    86 
    89     Examples:
    87     Examples:
    90 
    88 
    91       + Linux:
    89       + Linux:
    92         ```
    90         ```
    93         "isabelle.home": "/home/makarius/Isabelle2018"
    91         "isabelle.home": "/home/makarius/Isabelle"
    94         ```
    92         ```
    95 
    93 
    96       + Mac OS X:
    94       + Mac OS X:
    97         ```
    95         ```
    98         "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018"
    96         "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
    99         ```
    97         ```
   100 
    98 
   101       + Windows:
    99       + Windows:
   102         ```
   100         ```
   103         "isabelle.home": "C:\\Users\\makarius\\Isabelle2018"
   101         "isabelle.home": "C:\\Users\\makarius\\Isabelle"
   104         ```
   102         ```
   105 
   103 
   106   * Restart the VSCode application to ensure that all extensions are properly
   104   * Restart the VSCode application to ensure that all extensions are properly
   107   initialized and user settings are updated. Afterwards VSCode should know about
   105   initialized and user settings are updated. Afterwards VSCode should know about
   108   `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
   106   `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).