Closed UlfNorell closed 10 years ago
From andreas....@gmail.com on November 12, 2013 13:31:44
Should I push this? The modification of \defaultcolumn is certainly good.
For \AgdaIndent, I would not reduce the current space; I rather increased it to \newcommand{\AgdaIndent}[1]{\hspace*{1ex}}
I suggest to change only the \defaultcolumn, but I you think otherwise, I am fine with pushing the current patch (after all, it's your baby).
Status: InfoNeeded
From stevan.a...@gmail.com on November 13, 2013 09:42:29
I mainly opened the ticket so people who care can discuss it, and added the patch so there would be some content.
I agree that with the change to default column the indentation is too small and should be increased, however it seems to me that \;\; adds slightly more indentation than \hspace*{1ex}?
Out of curiosity are you using it for a (beamer) presentation or a document? Maybe we see spaces differently cause text size isn't the same? I've only used it for documents so far.
It's not a big difference between the two and I'm fine with either, the current \quad is not enough though I think.
From andreas....@gmail.com on November 13, 2013 16:01:00
Ah, yes, I am using beamer.cls. I also found that \quad is not enough. When I tested \;\; now, it seemed indeed sufficient (more than I expected, was not \; supposed to be half-a-space character?!).
Ok, I go ahead and push the patch.
Status: Fixed
From stevan.a...@gmail.com on November 12, 2013 17:56:33
As proposed in: http://comments.gmane.org/gmane.comp.lang.agda/5836 Do the following changes to agda.sty:
-\newcommand{\AgdaIndent}[1]{\quad} +\newcommand{\AgdaIndent}[1]{\;\;}
-\defaultcolumn{l} +\defaultcolumn{@{~}l@{~}}
Patch attached.
Attachment: agda-sty.patch
Original issue: http://code.google.com/p/agda/issues/detail?id=955