namespace+def+elab flips string highlighting

Julian / tree-sitter-lean

Experimental tree-sitter parser for the Lean (4) Theorem Prover

MIT License

28 stars 5 forks source link

namespace+def+elab flips string highlighting #4

Closed gebner closed 3 years ago

gebner commented 3 years ago

import Lean
namespace A

def a : Nat := 42

scoped elab "b" c:term " ← " d:term : term <= expectedType => do
  this line is highlighted as a string, but is regular code
  throwError " 42 "

scoped syntax "_qq_match" term " ← " term " | " doElem : term

Julian commented 3 years ago

Fixed I believe in 0b3ad7435397b9fc2e98d0803af84f52829249f4.