[Agda] Printing strings in the emacs mode

[Guillaume Brunerie]

Great, thanks, it works!

I had tried C-u C-u C-c C-n already but with the `show` in
Data.String, and somehow it printed even more escapes. But with `show
= id`, it works, thanks!

Guillaume

On Tue, Nov 21, 2017 at 12:39 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
> 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
>
>