OCaml

Lambda, arrows, logic, comparisons and Greek letters for OCaml, plus a few list functions as quantifiers. Requires an extension that provides the language id ocaml.

Where to put it

The rules go into your VS Code settings.json. Open the command palette (Ctrl+Shift+P) and run Preferences: Open User Settings (JSON) to enable them for all projects, or edit .vscode/settings.json to enable them for one workspace. Add an entry for this language to the prettifySymbols.substitutions array (if the setting already exists, add the entry to the existing array; entries for different languages sit side by side):

"prettifySymbols.substitutions": [
    {
        "language": "ocaml",
        "substitutions": [
            // paste the rules from below here
        ]
    }
]

Changes take effect as soon as you save settings.json. The extension is enabled by default; the animation at the bottom starts with it switched off only to show the difference.

Language setting

"language": "ocaml",

language selects the files the entry applies to: a language id as shown in the status bar at the bottom right of VS Code.

Rules

{ "ugly": "fun",            "pretty": "λ", "pre": "\\b", "post": "\\b" },
{ "ugly": "<-",             "pretty": "←" },
{ "ugly": "->",             "pretty": "→" },
{ "ugly": "=",              "pretty": "=", "pre": "[^<>=!]|^", "post": "[^<>=]|$" },
{ "ugly": "==",             "pretty": "≡" },
{ "ugly": "!=",             "pretty": "≢" },
{ "ugly": "<>",             "pretty": "≠" },
{ "ugly": "&&",             "pretty": "∧" },
{ "ugly": "\\|\\|",         "pretty": "∨" },
{ "ugly": "not\\s?",        "pretty": "¬", "pre": "\\b", "post": "\\b" },
{ "ugly": ">",              "pretty": ">", "pre": "[^=\\-<>]|^", "post": "[^=\\-<>]|$" },
{ "ugly": "<",              "pretty": "<", "pre": "[^=\\-<>]|^", "post": "[^=\\-<>]|$" },
{ "ugly": ">=",             "pretty": "≥", "pre": "[^=\\-<>]|^", "post": "[^=\\-<>]|$" },
{ "ugly": "<=",             "pretty": "≤", "pre": "[^=\\-<>]|^", "post": "[^=\\-<>]|$" },
{ "ugly": "sqrt\\s?",       "pretty": "√", "pre": "\\b", "post": "\\b" },
{ "ugly": "alpha",          "pretty": "α", "pre": "\\b", "post": "\\b" },
{ "ugly": "beta",           "pretty": "β", "pre": "\\b", "post": "\\b" },
{ "ugly": "gamma",          "pretty": "γ", "pre": "\\b", "post": "\\b" },
{ "ugly": "delta",          "pretty": "δ", "pre": "\\b", "post": "\\b" },
{ "ugly": "''",             "pretty": "″" },
{ "ugly": "'",              "pretty": "′" },
{ "ugly": "List[.]for_all", "pretty": "∀", "pre": "\\b", "post": "\\b" },
{ "ugly": "List[.]exists",  "pretty": "∃", "pre": "\\b", "post": "\\b" },
{ "ugly": "List[.]mem",     "pretty": "∈", "pre": "\\b", "post": "\\b" },
{ "ugly": "\\|",            "pretty": "║", "pre": "^\\s+" }

What is what

Each rule is one line: ugly is a regular expression for the text to hide, pretty is what is shown instead, and the optional pre and post are regular expressions that must match the text just before and after, without being replaced themselves. Backslashes are written twice because the value is parsed by JSON and then as a regular expression. See Settings for all fields.

• fun: λ, only as a whole word.
• ->, <-: →, ←.
• =, ==, !=, <>: the single = is replaced by itself, == (physical equality) becomes ≡, != becomes ≢ and <> (structural inequality) becomes ≠.
• &&, ||, not: ∧, ∨, ¬. not and sqrt swallow an optional following space, so not x becomes ¬x.
• >, <, >=, <=: comparisons. > and < are replaced by themselves; they are kept from the original page and can be removed. The pre/post classes keep >=, ->, <- and friends from being split into pieces.
• alpha, beta, gamma, delta: α β γ δ, only as whole words.
• ' and '': primes ′ and ″, e.g. x' and x''.
• List.for_all, List.exists, List.mem: ∀, ∃, ∈.
• | at the start of an indented line (pattern matching cases) becomes a vertical bar ║; pre: ^\\s+ restricts this to the beginning of a line so that || and bars inside expressions are left alone.

Note: symbol 'not identical to' (&#x2262 ≢) is not always rendered correctly in Chrome on Windows. Potential alternative: ⧥.

In action

The animation is rendered from the rules on this page. The code is never modified: clicking into a symbol (or moving the cursor onto it) shows the original text again, and the symbol returns when the cursor leaves.