Initial support for semantic highlights

[david-christiansen]

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.

[archaeron]

I think to change the text color instead of the background we'd need a dynamic Grammar https://atom.io/docs/api/v0.209.0/Grammar. I'm not entirely sure if that's possible. I found some entries on the atom forum of people who tried that and listed them here: https://github.com/idris-hackers/atom-language-idris/issues/10

[archaeron]

On windows I need this https://github.com/idris-hackers/atom-language-idris/pull/32 to pass this test: https://github.com/idris-hackers/atom-language-idris/pull/31/files#diff-e875356097b1d027706a2fa01ee6e6cbR134 because of the backslashes. :+1:

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 :(

[archaeron]

never mind. It does now. It looks terrible xD (sorry)

[archaeron]

it is great :) we might be able to extract the colors from the theme someone has installed and use those for the coloring.

[david-christiansen]

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.

[david-christiansen]

And yes, I know it's ugly - that's what I said!

[david-christiansen]

https://ensime.github.io/talks/scaladays15/#/8/2 is the screenshot I was thinking of

[archaeron]

i really appreciate this pull request and it's well done :smile:. I just wasn't prepared for all the colors :wink:

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. Another one that I like is the atom-fsharp package. They have a cool REPL implementation. https://pbs.twimg.com/tweet_video/CHK5qRpWgAA28ZU.mp4

[david-christiansen]

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.

[archaeron]

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?

[david-christiansen]

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.

[david-christiansen]

I should really update the screenshot gifs on the idris-mode readme soon - it just takes FOREVER to make UI gifs.

[archaeron]

thank you for explaining. It makes a lot of sense to have this. Do you think we should also try the dynamic grammar version so that we can style the text and compare it to this version and then choose? Or should we just go on with the highlight?

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.

[david-christiansen]

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 :browse and semantic highlights of source. If only time were unlimited.

[archaeron]

@david-christiansen sorry for not replying earlier. The exams have started. I will merge this as soon as I have merged https://github.com/idris-hackers/atom-language-idris/tree/optional-typecheck Sorry, should have done it before starting that one.

The videos and the gifs would help :) I'm trying to install your idris mode in emacs but didn't succeed yet.

[david-christiansen]

No rush with this thing. Perhaps we should coordinate in Prague?

[archaeron]

Yes please. And it would be great if you could help me install the emacs mode, if I can't manage to do it and show it to me. I'd like to steal some ideas from you. :)

[david-christiansen]

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.

[archaeron]

here http://melpa.org/#/getting-started it says that I need a package.el and that it should be bundled. (I have emacs 24.5). I've found my .emacs file and the .emacs.d folder, But I can't find package.el. Is there another folder where I might find that file?

[archaeron]

I have now pasted this into my .emacs file (I know it can't work, but I'm a bit lost here :D)

(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

[david-christiansen]

You should delete this bit:

(idris-mode
 :repo "idris-hackers/idris-mode"
 :fetcher github
 :files (:defaults "logo-small.png"))

That's kind of like the MELPA equivalent of a Makefile, not Emacs config. Then do M-x list-packages and install idris-mode. Then add (require 'idris-mode) to your init.el.

Does that make sense?

[david-christiansen]

Try this .emacs:

;;; Get MELPA
(require 'package)
(add-to-list 'package-archives
             '("melpa" . "http://melpa.org/packages/") t)
(add-to-list 'package-archives
             '("melpa-stable" . "http://stable.melpa.org/packages/") t)

(package-initialize)

;;; Handy loader for external packages
(unless (package-installed-p 'use-package)
  (package-refresh-contents)
  (package-install 'use-package))
(require 'use-package)

(use-package idris-mode
  :ensure t
  :config (remove-hook 'idris-mode-hook 'turn-on-eldoc-mode))

(add-to-list 'completion-ignored-extensions ".ibc")

[archaeron]

it's working perfectly, thanks a lot! I'll have to play with it a bit :)

[david-christiansen]

I'd love to hear your feedback about the interface as a new Emacs user!

[archaeron]

@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 :)

[david-christiansen]

Good to hear! See you soon!

[archaeron]

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 :)

[david-christiansen]

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.

[archaeron]

this is really cool! although probably both approaches are still needed, as someone said that the typechecking could be slow for large files. I've implemented print-definition and it shows how cool it looks with just compiler highlighting.

so this looks really interesting if fast enough.

EDIT: it still says type of in the title. but it's the definition.

[david-christiansen]

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 :)