Initial support for semantic highlights #31
Conversation
Semantic source highlighting information from Idris is no longer ignored. Atom highlights are not wrapped around the text. Instead, they live at a different z-index, which means they can't apply text highlights. This is why the selection doesn't touch text colors. Thus, the semantic highlights are applied to the background only. Because they are ugly, they are currently disabled by default in the settings. But it's a start that can be built upon.
|
I think to change the text color instead of the background we'd need a dynamic |
|
On windows I need this #32 to pass this test: https://github.com/idris-hackers/atom-language-idris/pull/31/files#diff-e875356097b1d027706a2fa01ee6e6cbR134 because of the backslashes. 👍 when I step through the code I can see that it now passes the test and executes: marker = editor.markBufferRange([start, end], invalidate: 'never')
decoration = editor.decorateMarker(marker, type: "highlight", class: semanticClass)
@semanticMarkers.push(marker)but it isn't marking anything. Maybe this explains why I couldn't get markers to work yesterday :( |
|
never mind. It does now. It looks terrible xD (sorry) |
|
it is great :) |
|
I haven't found a good way to use theme colors for Idris on Emacs. This is because most themes specify syntactic highlighting, rather than semantic. That is, they say how to highlight identifiers, keywords, operators, etc. But Idris highlighting is changing the color of identifiers based on what they point to. So most themes just lack the right bits, unless they have colors for Agda defined, which is where we got the feature from. I noticed that https://github.com/hedefalk/atom-ensime has a lot of feature like idris-mode for Emacs, like hovering things for type information. Perhaps you can re-use the code that they use? I also saw a screenshot where it looked like they were highlighting vars and vals differently, which means that there's semantic highlighting. It might be worth investigating which APIs they call. I won't likely do this due to other commitments - my goal here was really just to get the basics in place to help you out. |
|
And yes, I know it's ugly - that's what I said! |
|
https://ensime.github.io/talks/scaladays15/#/8/2 is the screenshot I was thinking of |
|
i really appreciate this pull request and it's well done 😄. I just wasn't prepared for all the colors 😉 Is there somewhere an explanation for the semantic highlighting? I don't quite understand it probably. Thank you for the link. I'll look at how they do their things. |
|
That does look nice! Something like that would be nice for Idris. The Idris REPL works a bit differently, in that you can't send it definitions the way you do in Lisp or F#. It's a bit more of the Racket or ghci style of working. The only explanation that I can think of is http://docs.idris-lang.org/en/latest/reference/repl.html#colours . The color says what kind of thing is referred to by the name: a type constructor, data constructor, function, etc. This makes it easier to see what things might compute and pattern match vs what things are known to be injective. |
|
So it doesn't just color an identifier with "identifier-color" as most of the highlighting in editors is, but it depends on what is inside it? |
|
Exactly - that's what makes it "semantic". This is really handy in dependently typed languages, because types, constructors, functions, and everything are all in one syntactic category. It's also nice in other settings, which is why e.g. Ensime does it for Scala, where you can see the difference between a class and its companion object or between mutable and immutable values. |
|
I should really update the screenshot gifs on the idris-mode readme soon - it just takes FOREVER to make UI gifs. |
|
thank you for explaining. It makes a lot of sense to have this. I downloaded a software to record my screen with the intention of making gifs of this package too. But I'd have to edit the videos so I have deferred that to package version 0.5 when things are more settled. |
|
TBH, I don't know what the best approach in Atom is. I would guess that the highlight one will be insufficient, due to the inability to change font properties in a highlight. But perhaps you can ask someone who really knows Atom well? The main thing I wanted to do with this PR was get the part where it talks to Idris to work, so that you could focus on the more Atom-facing bits. When I do screen GIFs it's with repeated screenshots rather than a recording program. That makes it easier to control things like how long it stays on one frame, etc. I'll do some new ones for Emacs soon. I should also update the videos on my YouTube channel to show |
|
@david-christiansen sorry for not replying earlier. The exams have started. The videos and the gifs would help :) I'm trying to install your idris mode in emacs but didn't succeed yet. |
|
No rush with this thing. Perhaps we should coordinate in Prague? |
|
Yes please. |
|
Sure thing. If you describe your difficulties in more detail, perhaps I can tell you how to set it up ahead of time. It should be as simple as setting up MELPA Stable and using the package interface, and if it's not, then it needs fixing. |
|
here http://melpa.org/#/getting-started it says that I need a |
|
I have now pasted this into my (require 'package) ;; You might already have this line
(add-to-list 'package-archives
'("melpa" . "http://melpa.org/packages/"))
(when (< emacs-major-version 24)
;; For important compatibility libraries like cl-lib
(add-to-list 'package-archives '("gnu" . "http://elpa.gnu.org/packages/")))
(idris-mode
:repo "idris-hackers/idris-mode"
:fetcher github
:files (:defaults "logo-small.png"))
(package-initialize) ;; You might already have this line |
|
You should delete this bit: That's kind of like the MELPA equivalent of a Makefile, not Emacs config. Then do Does that make sense? |
|
Try this |
|
it's working perfectly, thanks a lot! |
|
I'd love to hear your feedback about the interface as a new Emacs user! |
|
@david-christiansen terribly sorry for the long delay. It feels really good. I didn't know how to close a subwindows at first, but now it's working really well :) |
|
Good to hear! See you soon! |
|
I was especially impressed with the good mouse support of emacs and the idris-mode. I always thought emacs woul be a purely terminal based editor. And see you soon :) |
|
In case you want to do the dynamic grammar approach, I've rigged up Idris to highlight keywords and other bits of parser flotsam as it goes, so you should be able to dispense entirely with regexp highlighting. This means that it also highlights things like user-defined syntax, so it's going to be smarter than anything not in the compiler. |
|
this is really cool! although probably both approaches are still needed, as someone said that the typechecking could be slow for large files.
so this looks really interesting if fast enough. EDIT: |
|
This is really nice for the compiler output! We had that in the Emacs mode long before there was support for source code highlighting. In the upcoming release, all source code tokens should be highlighted, which will be nice :) |
|
All commands that display code are done with just the compiler highlighting :) And they look great! Ohoh, I just found this:
|
|
This seems like a major design problem in both Atom and TextMate - the inability of external tools to calculate highlighting for a file. It might be worth opening an issue with them to see if they can make the built-in regexp grammar optional, because custom highlighting as well as highlighting based on abstractions stronger than regexps are both broadly applicable. |
|
I've opened an issue for atom here: atom/atom#7989 |
|
Hi, there's another open issue that may be of interest here: atom/atom#8669 |
|
@altaic this is very interesting, thanks :) |
Semantic source highlighting information from Idris is no longer ignored.
Atom highlights are not wrapped around the text. Instead, they live at a different z-index, which means they can't apply text highlights. This is why the selection doesn't touch text colors. Thus, the semantic highlights are applied to the background only.
Because they are ugly, they are currently disabled by default in the settings. But it's a start that can be built upon.
This is my first CoffeeScript code ever, so sorry if it's doing something wrong.