search

banacorn / language-agda

Agda language support for the Atom editor
https://atom.io/packages/language-agda
MIT License
13 stars 5 forks source link

Fix typo #16

Closed buggymcbugfix closed 5 years ago

buggymcbugfix commented 5 years ago

Hey, I'm assuming that binging is a typo.

By the way, I'm also wondering why Atom doesn't seem to colour punctuation.X entities differently? I think it would be a bit nicer if type signatures weren't so monochrome.

banacorn commented 5 years ago

Thanks for this PR.

The way how Atom colour things is still much a mystery. I can only do so much as to read the documentation of TextMate (the legacy it built on) and see how other language packages are using them.

Another problem about the type signatures is that, types in Agda are not that special, comparing to other languages that possesses phase distinctions. If we are highlighting types then we are highlighting terms. And since most these things are user-defined, there's not many special things we can highlighting.

buggymcbugfix commented 5 years ago

The way how Atom colour things is still much a mystery.

Indeed! The lack of documentation is rather frustrating.

Another problem about the type signatures is that, types in Agda are not that special [...]

Yeah, of course. What I meant was literally just having different colours for reserved symbols like : and →, e.g. making those keywords in the tree sitter grammar gives something like the following:

screen shot 2018-10-17 at 10 26 39

I have no idea why the function arrows and forall aren't getting coloured though. It's not even due to Unicode, since -> and forall don't get coloured either.

My dream would be to base the syntax colouring on the compiler's type information, but I guess I'll have to dream on...

banacorn commented 5 years ago

I thought I had them covered, but apparently not. 😢 https://github.com/banacorn/language-agda/blob/12342c3d18bd9083aaeb2e9f06d2aec3304a2790/grammars/tree-sitter-agda.cson#L43-L51

It's actually possible to base the syntax colouring on the compiler's type information. That is what agda-mode on Emacs has been doing. But I threw those information away, and opted for the traditional static syntax highlighting (this repo), in fear of the performance implication that it may follow (dynamically layering hundreds of markers on the editor ), which is mere guesswork and completely unjustified.

I should give it a try!