forked from dwrensha/animate-lean-proofs
-
Notifications
You must be signed in to change notification settings - Fork 0
/
HighlightSyntax.lean
122 lines (100 loc) · 3.12 KB
/
HighlightSyntax.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
import Lean
namespace HighlightSyntax
/-- For each character index in the text, a
Nat represting the color at that index.
-/
abbrev ColorMap := Array Nat
def cat_to_color : String → Nat
| "Token.Text" => 1
| "Token.Text.Whitespace" => 2
| "Token.Keyword" => 3
| "Token.Name" => 4
| "Token.Name.Builtin.Pseudo" => 5
| "Token.Operator" => 6
| "Token.Literal.Number.Integer" => 7
| _ => 0
section parse
/-
This section is a lightly adapted copy of some stuff from Lean/Data/Json/Parser.lean.
-/
open Lean.Parsec
open Lean
namespace Parse
def hexChar : Parsec Nat := do
let c ← anyChar
if '0' ≤ c ∧ c ≤ '9' then
pure $ c.val.toNat - '0'.val.toNat
else if 'a' ≤ c ∧ c ≤ 'f' then
pure $ c.val.toNat - 'a'.val.toNat + 10
else if 'A' ≤ c ∧ c ≤ 'F' then
pure $ c.val.toNat - 'A'.val.toNat + 10
else
fail "invalid hex character"
def escapedChar : Parsec Char := do
let c ← anyChar
match c with
| '\\' => return '\\'
| '"' => return '"'
| '/' => return '/'
| 'b' => return '\x08'
| 'f' => return '\x0c'
| 'n' => return '\n'
| 'r' => return '\x0d'
| 't' => return '\t'
| 'u' =>
let u1 ← hexChar; let u2 ← hexChar; let u3 ← hexChar; let u4 ← hexChar
return Char.ofNat $ 4096*u1 + 256*u2 + 16*u3 + u4
| 'x' =>
let b1 ← hexChar; let b2 ← hexChar
return Char.ofNat $ 16*b1 + b2
| _ => fail "illegal \\u escape"
partial def strCore (acc : String) : Parsec String := do
let c ← peek!
if c = '"' then -- "
skip
return acc
else
let c ← anyChar
if c = '\\' then
strCore (acc.push (← escapedChar))
-- as to whether c.val > 0xffff should be split up and encoded with multiple \u,
-- the JSON standard is not definite: both directly printing the character
-- and encoding it with multiple \u is allowed. we choose the former.
else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then
strCore (acc.push c)
else
fail "unexpected character in string"
def str : Parsec String := strCore ""
end Parse
end parse
def assign_colors (s : String) : IO ColorMap := do
-- TODO randomize? or use stdio
let filename := "/tmp/animate-lean.txt"
IO.FS.writeFile filename s
let child ← IO.Process.spawn {
cmd := "pygmentize"
args := #["-l", "lean4", "-f", "raw", filename]
stdout := .piped
}
let output ← child.stdout.readToEnd
let exitCode ← child.wait
if exitCode != 0
then throw (IO.userError "pygmentize failed")
let mut result := #[]
let mut idx := 0
for line in output.split (· = '\n') do
if line = "" then continue
let [cat, val] := line.split (· = '\t') |
throw (IO.userError s!"bad pygmentize output: {line}")
let val' := (val.drop 1).dropRight 1 ++ "\""
match Parse.str val'.mkIterator with
| Lean.Parsec.ParseResult.success _ v =>
for _c in v.toList do
result := result.push (cat_to_color cat)
idx := idx + 1
| Lean.Parsec.ParseResult.error _ err =>
throw (IO.userError s!"failed to parse string {val}: {err}")
let _ := s.length
--dbg_trace "lengths : {s.length} vs {result.size}"
--dbg_trace result
return result