[Agda] Pretty Print Line Length

[Philip Wadler]

That's disappointing. Thanks for letting me know. Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 23 May 2018 at 17:07, Ulf Norell <ulf.norell at gmail.com> wrote:

> There's currently no option to change this. If you feel adventurous the
> pretty-print document is
> rendered here:
>
> https://github.com/agda/agda/blob/7b120057db1bca4bb304e3a77fb0fc
> 5ca1fb6ca1/src/full/Agda/Interaction/EmacsTop.hs#L139
>
> / Ulf
>
> On Wed, May 23, 2018 at 9:41 PM, Philip Wadler <wadler at inf.ed.ac.uk>
> wrote:
>
>> How does one adjust the length of the pretty-printed expression, e.g.,
>> when using ^C^N in Emacs mode? Apologies if this is obvious, but I could
>> not spot it in the documentation or with a Google search. Cheers, -- P
>>
>> .   \ Philip Wadler, Professor of Theoretical Computer Science,
>> .   /\ School of Informatics, University of Edinburgh
>> .  /  \ and Senior Research Fellow, IOHK
>> . http://homepages.inf.ed.ac.uk/wadler/
>>
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>> _______________________________________________
>> 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/20180524/bc267bf4/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180524/bc267bf4/attachment.ksh>