[Agda] Pretty Print Line Length

[Philip Wadler]

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/

[Ulf Norell]

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/7b120057db1bca4bb304e3a77fb0fc5ca1fb6ca1/src/full/Agda/Interaction/EmacsTop.hs#L139

/ Ulf

Post by Philip Wadler
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
https://lists.chalmers.se/mailman/listinfo/agda

[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/

Post by Ulf Norell
There's currently no option to change this. If you feel adventurous the
pretty-print document is
https://github.com/agda/agda/blob/7b120057db1bca4bb304e3a77fb0fc
5ca1fb6ca1/src/full/Agda/Interaction/EmacsTop.hs#L139
/ Ulf

Post by Philip Wadler
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
https://lists.chalmers.se/mailman/listinfo/agda