Lexical error with tab character in literate Agda text

[wadler]

Agda reports a lexical error when there is a tab in the source code, even if the tab appears in a commented-out part of the source.

[andreasabel]

Phil @wadler, would you attach a file with MWE? I cannot reproduce this, tabs in comments seem ok.

[nad]

@andreasabel, try putting the following text into Bug.lagda.md:

A tab character: '	'.

Result:

Bug.lagda.md:1,1: Lexical error (you may want to replace tabs with spaces):
<ERROR>
	  
...

[andreasabel]

The problem is that literate stuff in a .lagda file is bleached, meaning non-whitespace is replaced by space characters. However, tabs, being ws, are kept, failing the Agda lexer.

agda/src/full/Agda/Syntax/Parser/Literate.hs

Lines 124 to 136 in 78ea6d2

	illiterate :: [Layer] -> String
	illiterate xs = concat
	[ (if isCode layerRole then id else bleach) layerContent
	| Layer{layerRole, layerContent} <- xs
	]
	-- | Replaces non-space characters in a string with spaces.
	bleach :: String -> String
	bleach s = map go s
	where
	go c | isSpace c = c
	go _ = ' '

A fix would be to replace tabs by single spaces, that would preserve the character position.

[andreasabel]

A fix would be to replace tabs by single spaces, that would preserve the character position.

Implemented this in #5582.