{"action":"closed","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2304","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2304/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2304/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2304/events","html_url":"https://github.com/agda/agda/issues/2304","id":189455262,"number":2304,"title":"Support for multi-line string literals in the LaTeX backend","user":{"login":"gallais","id":1094905,"avatar_url":"https://avatars.githubusercontent.com/u/1094905?v=3","gravatar_id":"","url":"https://api.github.com/users/gallais","html_url":"https://github.com/gallais","followers_url":"https://api.github.com/users/gallais/followers","following_url":"https://api.github.com/users/gallais/following{/other_user}","gists_url":"https://api.github.com/users/gallais/gists{/gist_id}","starred_url":"https://api.github.com/users/gallais/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gallais/subscriptions","organizations_url":"https://api.github.com/users/gallais/orgs","repos_url":"https://api.github.com/users/gallais/repos","events_url":"https://api.github.com/users/gallais/events{/privacy}","received_events_url":"https://api.github.com/users/gallais/received_events","type":"User","site_admin":false},"labels":[{"id":245647317,"url":"https://api.github.com/repos/agda/agda/labels/bug","name":"bug","color":"fc2929","default":true},{"id":245649592,"url":"https://api.github.com/repos/agda/agda/labels/latex-backend","name":"latex-backend","color":"ededed","default":false}],"state":"closed","locked":false,"assignee":{"login":"gallais","id":1094905,"avatar_url":"https://avatars.githubusercontent.com/u/1094905?v=3","gravatar_id":"","url":"https://api.github.com/users/gallais","html_url":"https://github.com/gallais","followers_url":"https://api.github.com/users/gallais/followers","following_url":"https://api.github.com/users/gallais/following{/other_user}","gists_url":"https://api.github.com/users/gallais/gists{/gist_id}","starred_url":"https://api.github.com/users/gallais/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gallais/subscriptions","organizations_url":"https://api.github.com/users/gallais/orgs","repos_url":"https://api.github.com/users/gallais/repos","events_url":"https://api.github.com/users/gallais/events{/privacy}","received_events_url":"https://api.github.com/users/gallais/received_events","type":"User","site_admin":false},"assignees":[{"login":"gallais","id":1094905,"avatar_url":"https://avatars.githubusercontent.com/u/1094905?v=3","gravatar_id":"","url":"https://api.github.com/users/gallais","html_url":"https://github.com/gallais","followers_url":"https://api.github.com/users/gallais/followers","following_url":"https://api.github.com/users/gallais/following{/other_user}","gists_url":"https://api.github.com/users/gallais/gists{/gist_id}","starred_url":"https://api.github.com/users/gallais/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gallais/subscriptions","organizations_url":"https://api.github.com/users/gallais/orgs","repos_url":"https://api.github.com/users/gallais/repos","events_url":"https://api.github.com/users/gallais/events{/privacy}","received_events_url":"https://api.github.com/users/gallais/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/16","html_url":"https://github.com/agda/agda/milestones/2.5.2","labels_url":"https://api.github.com/repos/agda/agda/milestones/16/labels","id":1713715,"number":16,"title":"2.5.2","description":null,"creator":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"open_issues":31,"closed_issues":194,"state":"open","created_at":"2016-04-18T13:25:09Z","updated_at":"2016-11-21T10:13:48Z","due_on":null,"closed_at":null},"comments":1,"created_at":"2016-11-15T17:27:20Z","updated_at":"2016-11-21T10:13:48Z","closed_at":"2016-11-21T10:13:48Z","body":"Using a multi-line string literal leads to a broken TeX file. Here is an example:\r\n\r\n````agda\r\n\\documentclass{article}\r\n\\usepackage{agda}\r\n\\begin{document}\r\n\\begin{code}\r\nopen import Data.String\r\n\r\nargh =  \"Hello, \r\n\\       \\World!\"\r\n\\end{code}\r\n\\end{document}\r\n````\r\n\r\nleads to (focusing on the important part):\r\n\r\n````latex\r\n\\>\\AgdaFunction{argh} \\AgdaSymbol{=} \\<[8]%\r\n\\>[8]\\AgdaString{\"Hello, \\<\\\\\r\n\\>\\textbackslash{}       \\textbackslash{}World!\"}\\<%\r\n````\r\n\r\nI guess a possible fix would be to close `\\AgdaString` before a newline, reopen it afterwards and repeating the process until a non-escaped quotation mark is found?"}}
{"actor":{"display_login":"gallais"}}