Lean.tmbundle

A TextMate bundle for the Lean language. This is also used by github/linguist to syntax-highlight Lean code in github.com. Everytime github/linguist is newly released, github pulls the latest version of this repository.

How to Install

After installing TextMate2, please execute the following instructions:

mkdir -p ~/Library/Application\ Support/Avian/Bundles
cd ~/Library/Application\ Support/Avian/Bundles
git clone https://github.com/leanprover/Lean.tmbundle.git

How to Edit

• Open TextMate

• Bundles >> Edit Bundles

  

• Lean >> Language Grammars

  

• Note: TextMate saves grammar files (.tmLanguage) in Apple's PLIST format, which makes it very difficult to edit them outside of TextMate. It rejects to save any mal-formed/incomplete files. While saving grammar files, TextMate also clean up any comments inside of them.

Resources

• TextMate's documentation on language grammars: http://manual.macromates.com/en/language_grammars
• Test grammars using Lightshow: https://github-lightshow.herokuapp.com
  • Example: library/algebra/binary.lean