Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Text replicate, spaces #967

Merged
merged 5 commits into from Apr 26, 2020

Conversation

ari-becker
Copy link
Collaborator

Adds a function which generates Text with the number of spaces specified by the parameter.

I believe that this merits addition to the standard library because, when generating a configuration file with dhall text, it is common for configuration files to have significant whitespace (indentation etc.), and adding this function would make it significantly easier for users to generate precise amounts of whitespace in order to match downstream configuration format requirements.

@ari-becker ari-becker changed the title Add Text whitespaceGenerator Add Text generateWhitespace Apr 19, 2020
Copy link
Collaborator

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How about adding a more general function

Text/replicate : Natural -> Text -> Text

instead?

If we prefer to stick with this one, I'd suggest calling it Text/spaces.

@sjakobi
Copy link
Collaborator

sjakobi commented Apr 19, 2020

The implementation could also be slightly simplified by using Prelude.List.replicate.

@Gabriella439
Copy link
Contributor

Yeah, I also think a Text/replicate function would be great and should be easy to implement in terms of List/replicate and Text/concat

- change generateWhitespace to a combination of replicate, spaces
- use Prelude.List.replicate instead (simplified)
@ari-becker
Copy link
Collaborator Author

Cool, I've incorporated both of your feedback. I did decide to keep generateWhitespace (now spaces) as a separate function from replicate as I think that it's a common-enough use-case to merit inclusion as a distinct function.

@ari-becker ari-becker changed the title Add Text generateWhitespace Add Text replicate, spaces Apr 19, 2020
Copy link
Collaborator

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm slightly concerned about API bloat with spaces, but not too much.

Prelude/Text/replicate Outdated Show resolved Hide resolved
@ari-becker ari-becker merged commit 9cc2f1e into dhall-lang:master Apr 26, 2020
@ari-becker ari-becker deleted the add-whitespace-generator branch April 26, 2020 07:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants