{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1917","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/1917/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1917/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1917/events","html_url":"https://github.com/agda/agda/pull/1917","id":143410325,"number":1917,"title":"instead of complaining about goal markers being read-only delete the …","user":{"login":"drull95","id":1316928,"avatar_url":"https://avatars.githubusercontent.com/u/1316928?v=3","gravatar_id":"","url":"https://api.github.com/users/drull95","html_url":"https://github.com/drull95","followers_url":"https://api.github.com/users/drull95/followers","following_url":"https://api.github.com/users/drull95/following{/other_user}","gists_url":"https://api.github.com/users/drull95/gists{/gist_id}","starred_url":"https://api.github.com/users/drull95/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/drull95/subscriptions","organizations_url":"https://api.github.com/users/drull95/orgs","repos_url":"https://api.github.com/users/drull95/repos","events_url":"https://api.github.com/users/drull95/events{/privacy}","received_events_url":"https://api.github.com/users/drull95/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/emacs","name":"emacs","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/interaction","name":"interaction","color":"ededed"}],"state":"open","locked":false,"assignee":null,"assignees":[],"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":37,"closed_issues":114,"state":"open","created_at":"2016-04-18T13:25:09Z","updated_at":"2016-08-17T08:48:53Z","due_on":null,"closed_at":null},"comments":15,"created_at":"2016-03-25T02:39:29Z","updated_at":"2016-08-18T08:10:07Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/agda/agda/pulls/1917","html_url":"https://github.com/agda/agda/pull/1917","diff_url":"https://github.com/agda/agda/pull/1917.diff","patch_url":"https://github.com/agda/agda/pull/1917.patch"},"body":"…whole goal.\r\n\r\nI'm new to elisp so I don't know if this is up to standard."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/240653633","html_url":"https://github.com/agda/agda/pull/1917#issuecomment-240653633","issue_url":"https://api.github.com/repos/agda/agda/issues/1917","id":240653633,"user":{"login":"nad","id":293222,"avatar_url":"https://avatars.githubusercontent.com/u/293222?v=3","gravatar_id":"","url":"https://api.github.com/users/nad","html_url":"https://github.com/nad","followers_url":"https://api.github.com/users/nad/followers","following_url":"https://api.github.com/users/nad/following{/other_user}","gists_url":"https://api.github.com/users/nad/gists{/gist_id}","starred_url":"https://api.github.com/users/nad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nad/subscriptions","organizations_url":"https://api.github.com/users/nad/orgs","repos_url":"https://api.github.com/users/nad/repos","events_url":"https://api.github.com/users/nad/events{/privacy}","received_events_url":"https://api.github.com/users/nad/received_events","type":"User","site_admin":false},"created_at":"2016-08-18T08:10:07Z","updated_at":"2016-08-18T08:10:07Z","body":"> So if I type C-k somewhere in a hole, the \"end of line\" is the end of the hole.\r\n\r\nUnless there is a line break before the end of the hole?\r\n\r\n> If I am outside the hole, the hole should be treated as a single character. One backspace from after the hole deletes the hole and its entire contents, may it be pages long.\r\n>\r\n> Implement this!\r\n\r\nAt the moment we attach [modification hooks](https://www.gnu.org/software/emacs/manual/html_node/elisp/Overlay-Properties.html#index-modification_002dhooks-_0028overlay-property_0029) to goals. Feel free to try to use them to implement what you have in mind. Idea:\r\n\r\n* You can see if a command deletes (part of) one or both goal markers.\r\n\r\n* By checking the value of `point` you can see if the command was invoked from the inside or the outside of the goal."}}
{"actor":{"display_login":"nad"}}