Latex backend should not produce newlines at beginning and end of code block

[UlfNorell]

From andreas....@gmail.com on November 12, 2013 17:27:02

Given input

\begin{code} module Test where \end{code}

the Latex backend produces

\begin{code}><% \

\AgdaKeyword{module} \AgdaModule{Test} \AgdaKeyword{where}<% \ <\end{code}

but I would like to get

\begin{code}%

\AgdaKeyword{module} \AgdaModule{Test} \AgdaKeyword{where}<% \end{code}

The code environment can take care of initial and final spacing. As it is now, it is hard to get rid of the extra vertical spacing introduced by the backend. (I know only hacks, like \vspace{-5ex} or so.)

Nice tool, btw.

Original issue: http://code.google.com/p/agda/issues/detail?id=954

[UlfNorell]

From stevan.a...@gmail.com on November 13, 2013 09:19:59

I think the attached patch should fix this.

Does anyone happen to know how to get the old behaviour back by changing the code environment?

I tried putting \mbox{}\ at the beginning and end:

\renewenvironment{code} {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\mbox{}} {\mbox{}\endpboxed\par\noindent\ignorespacesafterend}

Which does something, I'm not sure if it's the same as the old behaviour though (need to do some more comparisons).

Labels: -Type-Enhancement Type-Patch

Attachment: agda-latex-spaces.patch

[UlfNorell]

From nils.anders.danielsson on November 13, 2013 09:29:58

Have you looked at the code in polycode.fmt?

[UlfNorell]

From stevan.a...@gmail.com on November 13, 2013 09:52:45

I have, but I don't understand it. Nor have I used lhs2TeX enough to know what it does. But yeah, it would probably be good if people who use lhs2TeX --agda are not surprised by the result produced by running agda --latex...

[UlfNorell]

From andreas....@gmail.com on November 13, 2013 16:09:08

I have not tested what you actually implemented, but black lines at start and end of code blocks could be honored. So, emit no empty lines for

\begin{code} Bla \end{code}

but do so for

\begin{code}

Bla

\end{code}

That means, only swallow the space after \begin{code} up to and including the NL character, and swallow the last NL plus spaces before the \end{code}.

Shall I push the patch or do you want to amend it?

Status: Started

[UlfNorell]

From andreas....@gmail.com on November 13, 2013 16:10:15

s/black/blank/

[UlfNorell]

From nils.anders.danielsson on November 14, 2013 02:04:15

I think we should follow the lhs2TeX approach, with different definitions of the code environment giving different results (see oldplainhscode, plainhscode and \sethscode in polycode.fmt). I also think that, by default, one should get reasonable layout. If I write

dkjasfkjasdfklajdfkl alsdfjdfj \begin{code} Foo : Set₁ Foo = Set \end{code} ölasdfjlasdfj ölasdfkjaölsdfjasdkfj,

then by default I would like to get reasonable spacing:

dkjasfkjasdfklajdfkl alsdfjdfj

Foo : Set₁
Foo = Set

ölasdfjlasdfj ölasdfkjaölsdfjasdkfj.

However, it should be possible to get less spacing by switching to a different code environment (as in \sethscode{oldplainhscode}).

[UlfNorell]

From stevan.a...@gmail.com on November 15, 2013 03:46:00

Andreas: Alright, I'm attaching an amended patch which hopefully does what you describe. I also added a test suite (the other patch).

Nisse: Perhaps open a new ticket for that?

Attachment: agda-latex-spaces3.patch agda-latex-backend-tests.patch

[UlfNorell]

From nils.anders.danielsson on November 15, 2013 06:13:50

I think that reasonable-looking code should, by default, be rendered in a reasonable way. If you have code inside a paragraph, then I would like to see spacing around the code:

Asdfjlasdjfklasdjf asödlfkjasdföklj asdöflkj öasdfklj asödfklj aösdfklj aösdfklj aösdfklj aösdlfkj asdfklj asdfkljdas fkjdöasfjdfjdkas fjkldasj fdfj öasfj dfj fjdfjöfjdkafja:

Foo : Set₁
Foo = Set

Asdfkljdkasjf öalsdfjdkjsf öasldfkjdkasjf öasldfkjdksfj öladfjkldasjf ölasdkjfdkasfj öldfjkldasjf ödkjsfkldjasf öljasdfklasjdfkldasf ölasdfjkldasjf öalsdfj ölasdfj asöklfj asdfkj dklsfj fj asdfjjfödkas fjdas föds dkasj fdaes fjdksfj ödklsf jask fdks föksd föklsd fdksj as fjdkas jfödkas fkas djfklasdj öklas.

Now, the question (for me) is what sort of code one should write to produce the formatted text above. LaTeX requires that there is no empty line before and after the code environment. We have at least two options:

• Without empty lines, as I do when I use lhs2TeX --poly:

  Asdfjlasdjfklasdjf asödlfkjasdföklj asdöflkj öasdfklj asödfklj aösdfklj aösdfklj aösdfklj aösdlfkj asdfklj asdfkljdas fkjdöasfjdfjdkas fjkldasj fdfj öasfj dfj fjdfjöfjdkafja: \begin{code} Foo : Set₁ Foo = Set \end{code} Asdfkljdkasjf öalsdfjdkjsf öasldfkjdkasjf öasldfkjdksfj öladfjkldasjf ölasdkjfdkasfj öldfjkldasjf ödkjsfkldjasf öljasdfklasjdfkldasf ölasdfjkldasjf öalsdfj ölasdfj asöklfj asdfkj dklsfj fj asdfjjfödkas fjdas föds dkasj fdaes fjdksfj ödklsf jask fdks föksd föklsd fdksj as fjdkas jfödkas fkas djfklasdj öklas.

• With empty lines in the code block:

  Asdfjlasdjfklasdjf asödlfkjasdföklj asdöflkj öasdfklj asödfklj aösdfklj aösdfklj aösdfklj aösdlfkj asdfklj asdfkljdas fkjdöasfjdfjdkas fjkldasj fdfj öasfj dfj fjdfjöfjdkafja: \begin{code}

  Foo : Set₁ Foo = Set

  \end{code} Asdfkljdkasjf öalsdfjdkjsf öasldfkjdkasjf öasldfkjdksfj öladfjkldasjf ölasdkjfdkasfj öldfjkldasjf ödkjsfkldjasf öljasdfklasjdfkldasf ölasdfjkldasjf öalsdfj ölasdfj asöklfj asdfkj dklsfj fj asdfjjfödkas fjdas föds dkasj fdaes fjdksfj ödklsf jask fdks föksd föklsd fdksj as fjdkas jfödkas fkas djfklasdj öklas.

I am not sure which option I prefer, but the first one is at least consistent with lhs2TeX --poly.

[UlfNorell]

From stevan.a...@gmail.com on November 15, 2013 08:26:07

I was quite happy with how it worked before this patch, i.e. if the lagda code looks like:

apa bepa cepa:

\begin{code} module M where \end{code}

depa epa fepa.

Then you get output which looks like:

apa bepa cepa:

module M where

depa epa fepa.

That's how I like to write (readable source code) and what I expect to output to be (readable pdf). But I understand that sometimes you might not want the space, as Andreas pointed out -- hence the change.

For the moment I just add the newline back using sed, e.g. s/begin{code}/begin{code}\n/, which seems to get back the old behaviour. The \mbox{}\ trick seems to work as well. Neither of those solutions seem optimal.

To me it seems natural that the following code:

apa bepa cepa: \begin{code} module M where \end{code} depa epa fepa.

Would produce:

apa bepa cepa: module M where depa epa fepa.

I.e. if you want to suppress the spacing in the output then suppress it in the input, but if that goes against lhs2TeX then I dunno.

In either way, this should be a agda.sty tweak rather than tweaking the compiler further?

[UlfNorell]

From nils.anders.danielsson on November 15, 2013 10:02:21

if the lagda code looks like:

apa bepa cepa:

\begin{code} module M where \end{code}

depa epa fepa.

Then you get output which looks like:

apa bepa cepa:

module M where

depa epa fepa.

Here you have three separate paragraphs. In many cases I want the code to be part of a paragraph, in which case I can't have blank lines before or after the code environment.

I realised now that my previous example was formatted incorrectly. The first line should be indented (assuming default settings for the article class):

Asdfjlasdjfklasdjf  asödlfkjasdföklj  asdöflkj  öasdfklj  asödfklj  <--- Indented.

aösdfklj aösdfklj aösdfklj aösdlfkj asdfklj asdfkljdas fkjdöasfjdfjdkas fjkldasj fdfj öasfj dfj fjdfjöfjdkafja:

Foo : Set₁
Foo = Set

Asdfkljdkasjf öalsdfjdkjsf öasldfkjdkasjf öasldfkjdksfj <--- Not indented. öladfjkldasjf ölasdkjfdkasfj öldfjkldasjf ödkjsfkldjasf öljasdfklasjdfkldasf ölasdfjkldasjf öalsdfj ölasdfj asöklfj asdfkj dklsfj fj asdfjjfödkas fjdas föds dkasj fdaes fjdksfj ödklsf jask fdks föksd föklsd fdksj as fjdkas jfödkas fkas djfklasdj öklas.

[UlfNorell]

From andreas....@gmail.com on November 15, 2013 11:16:06

My (original) concern was that there is no reasonable definition for the code environment (I would not consider negative spacing as reasonable) that would turn

bla bla \begin{code} module M where \end{code} bla bla

into just

bla bla module M where bla bla

If the LaTeX output does not insert beginning and ending newline, but the code-environment does this instead by default, that's fine with me (and, I guess, reasonable behavior).

[UlfNorell]

From andreas....@gmail.com on November 18, 2013 04:27:55

Pushed the latest patch.

Status: Fixed