[Agda] Agda on GitHub Atom

[Balaji Rao R]

On 14-Apr-2014, at 16:31, Helmut Grohne <grohne at cs.uni-bonn.de> wrote:

> On Sat, Apr 12, 2014 at 11:56:48PM +0530, Balaji Rao R wrote:
>> I’m interested to develop an Agda package for the GitHub Atom editor. Can anyone give me pointers on how to get started on the Agda side ? I would like to start by trying to get highlighting to work.
> 
> The basic issue is that the better syntax highlighting relies on type
> checking. I am aware of 4 ways to highlight Agda:
> 
> * Use agda --html or agda --latex (uses type checking).
> * Emacs agda2-mode (uses type checking by running agda in a separate
>   process).
> * Vim can use agda --vim output files for highlighting see
>   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing
>   (uses type checking), but one can also use the generic syntax file
>   without type checking to achieve very limited highlighting
> * lhs2TeX has very very limited highlighting (no type checking used for
>   highlighting).
> 
> In any case there is more to editing Agda than just highlighting.
> Working with "holes" and "goals" is essential. "Just" highlighting helps
> with reading Agda code, but is little help for writing.
> 
> http://oxij.org/note/BrutalDepTypes/ is one of the introductions that
> describes the process of editing in addition to describing the language.
> As far as I can tell the Emacs editing experience is currently unmatched
> by any other tool in the Agda world. 
> 

Thanks for the reply. I’ve used emacs agda2-mode quite a bit. I’m looking to replicate it on Atom.

I’ve seen that there are various files in Interaction/Highlighting, for example. I was looking for some broad guidelines regarding which file does what, just to help me get started.

- Balaji