Skip to content
Snippets Groups Projects
Commit ed3b52f9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'vscode-editor-docs' into 'master' 

Add VS code to the editor.md docs

See merge request iris/iris!397
parents 3f069634 b32af454
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 207 additions and 0 deletions
docs/editor.md
+ 207
− 0
View file @ ed3b52f9
......@@ -347,3 +347,210 @@ Here is a `coqide.bindings` file for a variety of symbols used in Iris:
\_v ᵥ
\_x ₓ
```
## Visual Studio Code
### VSCoq setup
The recommended extension as of December 2019 is [Maxime Dénès's
VScoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
Press `Ctrl Shift P` or `Cmd Shift P` and then type "coq" to see the list of Coq
commands and keyboard shortcuts.
### Font setup
To use unicode you need a font that supports all the symbols, such as [Fira
Code](https://github.com/tonsky/FiraCode/wiki/Installing). Download and install
the font, and in VS Code press `Cmd ,` or `Ctrl ,` to go to the settings, search
for "font", and use "FiraCode-Retina" as the font-family and optionally enable
ligatures.
### Unicode input setup
Install the [Generic input method
extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-input-method).
To insert a symbol, type the code for a symbol such as `\to` and then press
`Space` or `Tab`. To enable Iris unicode input support, open your user settings,
press `Cmd ,` or `Ctrl ,`, and type "generic-input-methods.input-methods", then
click on "Edit in settings.json" and add the following:
```
"generic-input-methods.input-methods": [
{
"name": "Iris Math",
"commandName": "text.math",
"languages": [
"coq"
],
"triggers": [
"\\"
],
"dictionary": [
// Standard LaTeX math notations
{ "label": "forall", "body": "∀", "description": "∀" },
{ "label": "exists", "body": "∃", "description": "∃" },
{ "label": "lam", "body": "λ", "description": "λ" },
{ "label": "not", "body": "¬", "description": "¬" },
{ "label": "->", "body": "→", "description": "→" },
{ "label": "<->", "body": "↔", "description": "↔" },
{ "label": "<-", "body": "←", "description": "←" },
{ "label": "==", "body": "≡", "description": "≡" },
{ "label": "/==", "body": "≢", "description": "≢" },
{ "label": "/=", "body": "≠", "description": "≠" },
{ "label": "neq", "body": "≠", "description": "≠" },
{ "label": "nequiv", "body": "≢", "description": "≢" },
{ "label": "<=", "body": "≤", "description": "≤" },
{ "label": "leq", "body": "≤", "description": "≤" },
{ "label": "in", "body": "∈", "description": "∈" },
{ "label": "notin", "body": "∉", "description": "∉" },
{ "label": "cup", "body": "∪", "description": "∪" },
{ "label": "cap", "body": "∩", "description": "∩" },
{ "label": "setminus", "body": "∖", "description": "∖" },
{ "label": "subset", "body": "⊂", "description": "⊂" },
{ "label": "subseteq", "body": "⊆", "description": "⊆" },
{ "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
{ "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
{ "label": "notsubseteq", "body": "⊈", "description": "⊈" },
{ "label": "meet", "body": "⊓", "description": "⊓" },
{ "label": "join", "body": "⊔", "description": "⊔" },
{ "label": "top", "body": "⊤", "description": "⊤" },
{ "label": "bottom", "body": "⊥", "description": "⊥" },
{ "label": "vdash", "body": "⊢", "description": "⊢" },
{ "label": "|-", "body": "⊢", "description": "⊢" },
{ "label": "dashv", "body": "⊣", "description": "⊣" },
{ "label": "Vdash", "body": "⊨", "description": "⊨" },
{ "label": "infty", "body": "∞", "description": "∞" },
{ "label": "comp", "body": "∘", "description": "∘" },
{ "label": "prf", "body": "↾", "description": "↾" },
{ "label": "bind", "body": "≫=", "description": "≫=" },
{ "label": "mapsto", "body": "↦", "description": "↦" },
{ "label": "hookrightarrow", "body": "↪", "description": "↪" },
{ "label": "uparrow", "body": "↑", "description": "↑" },
// Iris specific
{ "label": "fun", "body": "λ", "description": "λ" },
{ "label": "mult", "body": "⋅", "description": "⋅" },
{ "label": "ent", "body": "⊢", "description": "⊢" },
{ "label": "valid", "body": "✓", "description": "✓" },
{ "label": "diamond", "body": "◇", "description": "◇" },
{ "label": "box", "body": "□", "description": "□" },
{ "label": "bbox", "body": "■", "description": "■" },
{ "label": "later", "body": "▷", "description": "▷" },
{ "label": "pred", "body": "φ", "description": "φ" },
{ "label": "and", "body": "∧", "description": "∧" },
{ "label": "or", "body": "∨", "description": "∨" },
{ "label": "comp", "body": "∘", "description": "∘" },
{ "label": "ccomp", "body": "◎", "description": "◎" },
{ "label": "all", "body": "∀", "description": "∀" },
{ "label": "ex", "body": "∃", "description": "∃" },
{ "label": "to", "body": "→", "description": "→" },
{ "label": "sep", "body": "∗", "description": "∗" },
{ "label": "star", "body": "∗", "description": "∗" },
{ "label": "lc", "body": "⌜", "description": "⌜" },
{ "label": "rc", "body": "⌝", "description": "⌝" },
{ "label": "Lc", "body": "⎡", "description": "⎡" },
{ "label": "Rc", "body": "⎤", "description": "⎤" },
{ "label": "empty", "body": "∅", "description": "∅" },
{ "label": "Lam", "body": "Λ", "description": "Λ" },
{ "label": "Sig", "body": "Σ", "description": "Σ" },
{ "label": "-", "body": "∖", "description": "∖" },
{ "label": "aa", "body": "●", "description": "●" },
{ "label": "af", "body": "◯", "description": "◯" },
{ "label": "auth", "body": "●", "description": "●" },
{ "label": "frag", "body": "◯", "description": "◯" },
{ "label": "iff", "body": "↔", "description": "↔" },
{ "label": "gname", "body": "γ", "description": "γ" },
{ "label": "incl", "body": "≼", "description": "≼" },
{ "label": "latert", "body": "▶", "description": "▶" },
{ "label": "update", "body": "⇝", "description": "⇝" },
{ "label": "bind", "body": "≫=", "description": "≫=" },
// accents (for iLöb)
{ "label": "\"o", "body": "ö", "description": "ö" },
// subscripts and superscripts
{ "label": "^^+", "body": "⁺", "description": "⁺" },
{ "label": "__+", "body": "₊", "description": "₊" },
{ "label": "^^-", "body": "⁻", "description": "⁻" },
{ "label": "__0", "body": "₀", "description": "₀" },
{ "label": "__1", "body": "₁", "description": "₁" },
{ "label": "__2", "body": "₂", "description": "₂" },
{ "label": "__3", "body": "₃", "description": "₃" },
{ "label": "__4", "body": "₄", "description": "₄" },
{ "label": "__5", "body": "₅", "description": "₅" },
{ "label": "__6", "body": "₆", "description": "₆" },
{ "label": "__7", "body": "₇", "description": "₇" },
{ "label": "__8", "body": "₈", "description": "₈" },
{ "label": "__9", "body": "₉", "description": "₉" },
{ "label": "__a", "body": "ₐ", "description": "ₐ" },
{ "label": "__e", "body": "ₑ", "description": "ₑ" },
{ "label": "__h", "body": "ₕ", "description": "ₕ" },
{ "label": "__i", "body": "ᵢ", "description": "ᵢ" },
{ "label": "__k", "body": "ₖ", "description": "ₖ" },
{ "label": "__l", "body": "ₗ", "description": "ₗ" },
{ "label": "__m", "body": "ₘ", "description": "ₘ" },
{ "label": "__n", "body": "ₙ", "description": "ₙ" },
{ "label": "__o", "body": "ₒ", "description": "ₒ" },
{ "label": "__p", "body": "ₚ", "description": "ₚ" },
{ "label": "__r", "body": "ᵣ", "description": "ᵣ" },
{ "label": "__s", "body": "ₛ", "description": "ₛ" },
{ "label": "__t", "body": "ₜ", "description": "ₜ" },
{ "label": "__u", "body": "ᵤ", "description": "ᵤ" },
{ "label": "__v", "body": "ᵥ", "description": "ᵥ" },
{ "label": "__x", "body": "ₓ", "description": "ₓ" },
// Greek alphabet
{ "label": "Alpha", "body": "Α", "description": "Α" },
{ "label": "alpha", "body": "α", "description": "α" },
{ "label": "Beta", "body": "Β", "description": "Β" },
{ "label": "beta", "body": "β", "description": "β" },
{ "label": "Gamma", "body": "Γ", "description": "Γ" },
{ "label": "gamma", "body": "γ", "description": "γ" },
{ "label": "Delta", "body": "Δ", "description": "Δ" },
{ "label": "delta", "body": "δ", "description": "δ" },
{ "label": "Epsilon", "body": "Ε", "description": "Ε" },
{ "label": "epsilon", "body": "ε", "description": "ε" },
{ "label": "Zeta", "body": "Ζ", "description": "Ζ" },
{ "label": "zeta", "body": "ζ", "description": "ζ" },
{ "label": "Eta", "body": "Η", "description": "Η" },
{ "label": "eta", "body": "η", "description": "η" },
{ "label": "Theta", "body": "Θ", "description": "Θ" },
{ "label": "theta", "body": "θ", "description": "θ" },
{ "label": "Iota", "body": "Ι", "description": "Ι" },
{ "label": "iota", "body": "ι", "description": "ι" },
{ "label": "Kappa", "body": "Κ", "description": "Κ" },
{ "label": "kappa", "body": "κ", "description": "κ" },
{ "label": "Lamda", "body": "Λ", "description": "Λ" },
{ "label": "lamda", "body": "λ", "description": "λ" },
{ "label": "Lambda", "body": "Λ", "description": "Λ" },
{ "label": "lambda", "body": "λ", "description": "λ" },
{ "label": "Mu", "body": "Μ", "description": "Μ" },
{ "label": "mu", "body": "μ", "description": "μ" },
{ "label": "Nu", "body": "Ν", "description": "Ν" },
{ "label": "nu", "body": "ν", "description": "ν" },
{ "label": "Xi", "body": "Ξ", "description": "Ξ" },
{ "label": "xi", "body": "ξ", "description": "ξ" },
{ "label": "Omicron", "body": "Ο", "description": "Ο" },
{ "label": "omicron", "body": "ο", "description": "ο" },
{ "label": "Pi", "body": "Π", "description": "Π" },
{ "label": "pi", "body": "π", "description": "π" },
{ "label": "Rho", "body": "Ρ", "description": "Ρ" },
{ "label": "rho", "body": "ρ", "description": "ρ" },
{ "label": "Sigma", "body": "Σ", "description": "Σ" },
{ "label": "sigma", "body": "σ", "description": "σ" },
{ "label": "Tau", "body": "Τ", "description": "Τ" },
{ "label": "tau", "body": "τ", "description": "τ" },
{ "label": "Upsilon", "body": "Υ", "description": "Υ" },
{ "label": "upsilon", "body": "υ", "description": "υ" },
{ "label": "Phi", "body": "Φ", "description": "Φ" },
{ "label": "phi", "body": "φ", "description": "φ" },
{ "label": "Chi", "body": "Χ", "description": "Χ" },
{ "label": "chi", "body": "χ", "description": "χ" },
{ "label": "Psi", "body": "Ψ", "description": "Ψ" },
{ "label": "psi", "body": "ψ", "description": "ψ" },
{ "label": "Omega", "body": "Ω", "description": "Ω" },
{ "label": "omega", "body": "ω", "description": "ω" }
]
}
]
```
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment