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

Document string literals #1756

Merged
merged 3 commits into from
Jul 19, 2021

Conversation

andrevidela
Copy link
Collaborator

#555, #1027, #1029 have been implemented, but the documentation and the changelog weren't updated at the same time. Documenting those feature is the last item in their todo list.

The features seem to work well except for #1755 and #1132 which are fairly innocuous.

@gallais gallais added documentation Improvements or additions to documentation language: literals labels Jul 19, 2021
.. code-block::

markdownExample : String
markdownExample = ##"markdown titles look like this: \##n"# Title \##n body""##
Copy link
Member

Choose a reason for hiding this comment

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

I'm confused: why do you have \##n instead of \n?
According to the next example using a multiline string you do want the newline?

Copy link
Collaborator Author

@andrevidela andrevidela Jul 19, 2021

Choose a reason for hiding this comment

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

Yes I do want the newline. You need to use \##n Because the escape sequence is \## in that string, if you were to write \n the text \n would appear instead of a new line.

Copy link
Member

Choose a reason for hiding this comment

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

I see. I always understood \n as a single character, not as n being escaped to mean newline. 🤔

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

the character n preceeded with the escape sequence renders a single character, just like \t, \r, \0. Raw strings allow the user to type those character without having to escape the \ character. But you can recover their meaning by using the \# escape sequence inside a raw string (or however many # you're using for the raw string)

docs/source/reference/strings.rst Outdated Show resolved Hide resolved
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
@andrevidela andrevidela merged commit ada33b9 into idris-lang:master Jul 19, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation language: literals
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants