8ea5742 · helix · git.iko.soy

.gitmodules+4

compare with master

unifiedsplit

@@ -190,6 +190,10 @@

190 path = helix-syntax/languages/tree-sitter-git-rebase

191 url = https://github.com/the-mikedavis/tree-sitter-git-rebase.git

192 shallow = true

193+[submodule "helix-syntax/languages/tree-sitter-lean"]

194+ path = helix-syntax/languages/tree-sitter-lean

195+ url = https://github.com/Julian/tree-sitter-lean

196+ shallow = true

193[submodule "helix-syntax/languages/tree-sitter-regex"]

197[submodule "helix-syntax/languages/tree-sitter-regex"]

194 path = helix-syntax/languages/tree-sitter-regex

198 path = helix-syntax/languages/tree-sitter-regex

195 url = https://github.com/tree-sitter/tree-sitter-regex.git

199 url = https://github.com/tree-sitter/tree-sitter-regex.git

book/src/generated/lang-support.md+1

@@ -24,6 +24,7 @@

24| json | ✓ | | ✓ | |

25| julia | ✓ | | | `julia` |

26| latex | ✓ | | | |

27+| lean | ✓ | | | `lean` |

27| ledger | ✓ | | | |

28| ledger | ✓ | | | |

28| llvm | ✓ | ✓ | ✓ | |

29| llvm | ✓ | ✓ | ✓ | |

29| llvm-mir | ✓ | ✓ | ✓ | |

30| llvm-mir | ✓ | ✓ | ✓ | |

helix-syntax/languages/tree-sitter-leannew file+1

Submodule changed.

languages.toml+11

@@ -241,6 +241,17 @@ comment-token = "%"

241

242indent = { tab-width = 4, unit = "\t" }

243

244+[[language]]

245+name = "lean"

246+scope = "source.lean"

247+injection-regex = "lean"

248+file-types = ["lean"]

249+roots = [ "lakefile.lean" ]

250+comment-token = "--"

251+language-server = { command = "lean", args = [ "--server" ] }

252+

253+indent = { tab-width = 2, unit = " " }

254+

244[[language]]

255[[language]]

245name = "julia"

256name = "julia"

246scope = "source.julia"

257scope = "source.julia"

runtime/queries/lean/folds.scmnew file+15

@@ -0,0 +1,15 @@

1+[

2+ (namespace)

3+ (section)

4+

5+ (instance)

6+ (def)

7+ (theorem)

8+ (example)

9+

10+ (product)

11+ (array)

12+ (list)

13+

14+ (string)

15+] @fold

runtime/queries/lean/highlights.scmnew file+217

@@ -0,0 +1,217 @@

1+(open

2+ namespace: (identifier) @namespace)

3+(namespace

4+ name: (identifier) @namespace)

5+(section

6+ name: (identifier) @namespace)

7+

8+;; Identifier naming conventions

9+((identifier) @type

10+ (#match? @type "^[A-Z]"))

11+

12+(arrow) @type

13+(product) @type

14+

15+;; Declarations

16+

17+[

18+ "abbrev"

19+ "def"

20+ "theorem"

21+ "constant"

22+ "instance"

23+ "axiom"

24+ "example"

25+ "inductive"

26+ "structure"

27+ "class"

28+

29+ "deriving"

30+

31+ "section"

32+ "namespace"

33+] @keyword

34+

35+(attributes

36+ (identifier) @function)

37+

38+(abbrev

39+ name: (identifier) @type)

40+(def

41+ name: (identifier) @function)

42+(theorem

43+ name: (identifier) @function)

44+(constant

45+ name: (identifier) @type)

46+(instance

47+ name: (identifier) @function)

48+(instance

49+ type: (identifier) @type)

50+(axiom

51+ name: (identifier) @function)

52+(structure

53+ name: (identifier) @type)

54+(structure

55+ extends: (identifier) @type)

56+

57+(where_decl

58+ type: (identifier) @type)

59+

60+(proj

61+ name: (identifier) @field)

62+

63+(binders

64+ type: (identifier) @type)

65+

66+["if" "then" "else"] @keyword.control.conditional

67+

68+["for" "in" "do"] @keyword.control.repeat

69+

70+(import) @include

71+

72+; Tokens

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+] @operator

117+

118+[

119+ "@&"

120+] @operator

121+

122+[

123+ "attribute"

124+ "by"

125+ "end"

126+ "export"

127+ "extends"

128+ "fun"

129+ "let"

130+ "have"

131+ "match"

132+ "open"

133+ "return"

134+ "universe"

135+ "variable"

136+ "where"

137+ "with"

138+ "λ"

139+ (hash_command)

140+ (prelude)

141+ (sorry)

142+] @keyword

143+

144+[

145+ "prefix"

146+ "infix"

147+ "infixl"

148+ "infixr"

149+ "postfix"

150+ "notation"

151+ "macro_rules"

152+ "syntax"

153+ "elab"

154+ "builtin_initialize"

155+] @keyword

156+

157+[

158+ "noncomputable"

159+ "partial"

160+ "private"

161+ "protected"

162+ "unsafe"

163+] @keyword

164+

165+[

166+ "apply"

167+ "exact"

168+ "rewrite"

169+ "rw"

170+ "simp"

171+ (trivial)

172+] @keyword

173+

174+[

175+ "catch"

176+ "finally"

177+ "try"

178+] @exception

179+

180+((apply

181+ name: (identifier) @exception)

182+ (#match? @exception "throw"))

183+

184+[

185+ "unless"

186+ "mut"

187+] @keyword

188+

189+[(true) (false)] @boolean

190+

191+(number) @constant.numeric.integer

192+(float) @constant.numeric.float

193+

194+(comment) @comment

195+(char) @character

196+(string) @string

197+(interpolated_string) @string

198+; (escape_sequence) @string.escape

199+

200+; Reset highlighing in string interpolation

201+(interpolation) @none

202+

203+(interpolation

204+ "{" @punctuation.special

205+ "}" @punctuation.special)

206+

207+["(" ")" "[" "]" "{" "}" "⟨" "⟩"] @punctuation.bracket

208+

209+["|" "," "." ":" ";"] @punctuation.delimiter

210+

211+(sorry) @error

212+

213+;; Error

214+(ERROR) @error

215+

216+; Variables

217+(identifier) @variable

runtime/queries/lean/injections.scmnew file+2

@@ -0,0 +1,2 @@

1+((comment) @injection.content

2+ (#set! injection.language "markdown"))

runtime/queries/lean/locals.scmnew file+5

@@ -0,0 +1,5 @@

1+[

2+ (module)

3+ (namespace)

4+ (section)

5+] @local.scope