{"comment":{"url":"https://api.github.com/repos/marsam/idris-mode/comments/13735584","html_url":"https://github.com/marsam/idris-mode/commit/0f2cafabec8b8cc824ff0b33374bbbaaf0518446#commitcomment-13735584","id":13735584,"user":{"login":"david-christiansen","id":115330,"avatar_url":"https://avatars.githubusercontent.com/u/115330?v=3","gravatar_id":"","url":"https://api.github.com/users/david-christiansen","html_url":"https://github.com/david-christiansen","followers_url":"https://api.github.com/users/david-christiansen/followers","following_url":"https://api.github.com/users/david-christiansen/following{/other_user}","gists_url":"https://api.github.com/users/david-christiansen/gists{/gist_id}","starred_url":"https://api.github.com/users/david-christiansen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/david-christiansen/subscriptions","organizations_url":"https://api.github.com/users/david-christiansen/orgs","repos_url":"https://api.github.com/users/david-christiansen/repos","events_url":"https://api.github.com/users/david-christiansen/events{/privacy}","received_events_url":"https://api.github.com/users/david-christiansen/received_events","type":"User","site_admin":false},"position":6,"line":161,"path":"inferior-idris.el","commit_id":"0f2cafabec8b8cc824ff0b33374bbbaaf0518446","created_at":"2015-10-13T09:32:49Z","updated_at":"2015-10-13T09:32:49Z","body":"I think there should be a comment here explaining why this is guarded. Something like:\r\n\"Idris sometimes prints a warning prior to the port number, which causes `string-match' to return 0\"\r\n\r\nIt is probably also a good idea to forward these warnings onward to the user - something like:\r\n```\r\n(if (string-match \"^\\\\s-*\\\\([0-9]+\\\\)\" string)\r\n    (idris-connect (string-to-number string))\r\n  (message \"Warning from Idris: %s\" string))\r\n```\r\n\r\nThe slightly stricter regexp matches the strings accepted by `string-to-number` anyway, so the `match-string` shouldn't be necessary, though it might be more clear anyway. I'm a bit concerned that `\"\\\\([0-9]+\\\\)\"` will end up matching a number in a warning printed by Idris."}}