[Agda] Agda on GitHub Atom

[Nils Anders Danielsson]

On 2014-04-14 20:09, Balaji Rao R wrote:
> 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.

If your goal is to use highlighting information, then the starting point
may be the type HighlightingInfo in
Agda.Interaction.Highlighting.Precise. The type checker stores
highlighting info in the state. For an example of how one can use the
highlighting info, take a look at, say,
Agda.Interaction.Highlighting.HTML.generateHTML, which is called from
Agda.Main.

-- 
/NAD