Compose key sequences for Lean

Stream: general

[Anthony Wang]

I wrote a simple and ugly script to convert the VSCode Lean input sequences to the XCompose format for typing these special characters outside of VSCode:

import Std.Data.HashMap
import Lean.Data.Json.Parser

def ofHex a b := let f (x : Char) := x.toNat - (if x.toNat ≤ '9'.toNat then '0'.toNat else 'a'.toNat - 10)
  16 * (f a) + (f b) |> Char.ofNat

def main := do
  let keysym := (← IO.FS.readFile "keysymdef.h").splitOn "\n" |>.map (fun l : String ↦ (ofHex (String.Pos.Raw.get! l ⟨45⟩) (String.Pos.Raw.get! l ⟨46⟩), Substring.mk l ⟨11⟩ ⟨30⟩ |>.takeWhile (· ≠ ' ') |>.toString)) |> Std.HashMap.ofList
  IO.println "include \"%L\""
  let raw_abbrs ← IO.Process.run { cmd := "curl", args := #["https://raw.githubusercontent.com/vasnesterov/vscode-lean4/refs/heads/master/lean4-unicode-input/src/abbreviations.json"] }
  match Lean.Json.parse raw_abbrs with
  | .ok (.obj abbrs) =>
    for abbr in abbrs do
      match abbr.2 with
      | .str s =>
        if !(s.contains '$') then
          -- XCompose doesn't like sequences to be prefixes of other sequences, so append enter to the end
          IO.println s!"<Multi_key> <{abbr.1.toList.map (keysym.get! ·) |> "> <".intercalate}> <Return> : \"{s.replace "\\" "\\\\"}\""
      | _ => pure ()
  | _ => IO.println "parse failure"

For instance, to type ↦, you would press Compose m a enter. To use this, download
.XCompose and move it to ~/.XCompose. I tested it on Linux but it should probably also work on Windows using WinCompose.

(Also here's keysymdef.h for converting from ASCII to X11 keysyms, which is used in my script above)

[Eric Paul]

Cool, this motivated me to set up something similar for mac based off your code, thanks for sharing it and the idea!