1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36

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.lines "keysymdef.h") |>.map
        (fun l : String ↦
          (ofHex (String.Pos.Raw.get! l ⟨45⟩) (String.Pos.Raw.get! l ⟨46⟩),
            Substring.Raw.mk l ⟨11⟩ ⟨30⟩ |>.takeWhile (· ≠ ' ') |>.toString)) |>
      Std.HashMap.ofArray
  IO.println "# Generated by https://git.unnamed.website/miscelleaneous/tree/Compose.lean"
  IO.println "include \"%L\""
  let raw_abbrs ←
    IO.Process.run
        { cmd := "curl",
          args :=
            #["https://raw.githubusercontent.com/leanprover/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"