[Agda] Printing strings in the emacs mode

[Ulf Norell]

You can use C-u C-u C-c C-n. This normalises `show TERM` and
prints the resulting string without quotes and escapes. It grabs
whatever `show` happens to be in scope, so in your case you could
define `show = id`.

/ Ulf

On Tue, Nov 21, 2017 at 3:37 AM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> Hi all,
>
> I’m using an Agda program to generate some Agda code. I’m not using
> reflection, I’m just using Agda as a regular functional programming
> language to generate strings, that I then want to copy-paste in a
> different file.
>
> For now, I didn’t bother with compilation, so I’m just defining terms
> of type String (from the standard library), and then I use C-c C-n in
> order to get their normal form.
>
> My problem is that in the result of C-c C-n, the string is surrounded
> by quotes, and the new lines are escaped as \n, which makes it a bit
> annoying to copy-paste, as I have to do a search and replace
> afterwards.
>
> Is there a way to use something like C-c C-n in order to get the
> normal form of a term of type String, but have it printed properly,
> without escaping the new lines and without the quotes before and
> after?
>
> Thanks,
> Best,
> Guillaume
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171121/fca5910a/attachment.html>