[Agda] Printing strings in the emacs mode

[Andreas Abel]

Just to remind the world, Haskell's "show" prints the *Haskell* 
representation of data.  (Usually the AST.)

Thus, extra escapes when showing strings.

--Andreas, keeper of law and order

On 21.11.2017 14:09, Guillaume Brunerie wrote:
> 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
>>
>>
> _______________________________________________
> 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://www.cse.chalmers.se/~abela/