[Agda] Agda and Emacs mode

[Jon Sterling]

Andrej,

I don't know what's intended for your student's project, but let me
say—an editing interface for Agda like Nuprl's (or even ALF's?) would be
really, really cool.

Kind regards,
Jon


On Tue, Dec 9, 2014, at 01:03 PM, Andreas Abel wrote:
> s/agda-setup/agda-mode/
> 
> On 09.12.2014 19:59, Andrea Vezzosi wrote:
> > There is some documentation on the commands agda --interaction accepts:
> >
> > https://github.com/agda/agda/blob/master/src/full/Agda/Interaction/InteractionTop.hs#L285
> >
> > The concrete syntax should be easy to figure out by looking at the
> > emacs buffer *agda2* during/after an agda session.
> >
> > The responses are printed out as s-expressions, which should make them
> > easy to parse in general.
> > Patching agda to optionally produce the output in some other format
> > shouldn't be hard either, it's a matter of writing a different pretty
> > printer for the Response type:
> > https://github.com/agda/agda/blob/master/src/full/Agda/Interaction/Response.hs#L37
> >
> > So overall it needs some amount of reverse engineering but not too bad?
> >
> > Only agda-setup should require an emacs installation, its job is to
> > setup the emacs mode though.
> >
> > Cheers,
> > Andrea
> >
> > On Tue, Dec 9, 2014 at 12:27 PM, Andrej Bauer <andrej.bauer at andrej.com> wrote:
> >> I have a master's student who would like to write a GUI for Agda on
> >> OSX (well, was told to do so).
> >>
> >> I suggested that he should just hook into Agda's communication with
> >> Emacs. Is there reasonable documentation on how Agda communicates with
> >> Emacs?
> >>
> >> Also, he now tells me that the Agda executable presupposes the
> >> existence of Emacs, which I have a hard time believing.
> >>
> >> Can someone shed some light on how realistic a project this is?
> >>
> >> With kind regards,
> >>
> >> Andrej
> >> _______________________________________________
> >> Agda mailing list
> >> Agda at lists.chalmers.se
> >> https://lists.chalmers.se/mailman/listinfo/agda
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda