{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/766","labels_url":"https://api.github.com/repos/leanprover/lean/issues/766/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/766/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/766/events","html_url":"https://github.com/leanprover/lean/issues/766","id":98909197,"number":766,"title":"autocompletion for `import`","user":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars.githubusercontent.com/u/2778936?v=3","gravatar_id":"","url":"https://api.github.com/users/leodemoura","html_url":"https://github.com/leodemoura","followers_url":"https://api.github.com/users/leodemoura/followers","following_url":"https://api.github.com/users/leodemoura/following{/other_user}","gists_url":"https://api.github.com/users/leodemoura/gists{/gist_id}","starred_url":"https://api.github.com/users/leodemoura/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leodemoura/subscriptions","organizations_url":"https://api.github.com/users/leodemoura/orgs","repos_url":"https://api.github.com/users/leodemoura/repos","events_url":"https://api.github.com/users/leodemoura/events{/privacy}","received_events_url":"https://api.github.com/users/leodemoura/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/leanprover/lean/labels/bug","name":"bug","color":"fc2929"},{"url":"https://api.github.com/repos/leanprover/lean/labels/emacs","name":"emacs","color":"eb6420"}],"state":"open","locked":false,"assignee":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"milestone":null,"comments":17,"created_at":"2015-08-04T07:48:43Z","updated_at":"2015-08-06T04:48:55Z","closed_at":null,"body":"I think autocompletion for `import` doesn't work anymore.\r\nExample: open empty `.lean` file and type\r\n```lean\r\nimport data\r\n```\r\nand press `<TAB>`. Emacs freezes for me. I have to press `Ctrl-g`.\r\n\r\n@avigad does it work for you?\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/128237428","html_url":"https://github.com/leanprover/lean/issues/766#issuecomment-128237428","issue_url":"https://api.github.com/repos/leanprover/lean/issues/766","id":128237428,"user":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars.githubusercontent.com/u/2778936?v=3","gravatar_id":"","url":"https://api.github.com/users/leodemoura","html_url":"https://github.com/leodemoura","followers_url":"https://api.github.com/users/leodemoura/followers","following_url":"https://api.github.com/users/leodemoura/following{/other_user}","gists_url":"https://api.github.com/users/leodemoura/gists{/gist_id}","starred_url":"https://api.github.com/users/leodemoura/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leodemoura/subscriptions","organizations_url":"https://api.github.com/users/leodemoura/orgs","repos_url":"https://api.github.com/users/leodemoura/repos","events_url":"https://api.github.com/users/leodemoura/events{/privacy}","received_events_url":"https://api.github.com/users/leodemoura/received_events","type":"User","site_admin":false},"created_at":"2015-08-06T04:48:55Z","updated_at":"2015-08-06T04:48:55Z","body":"Here is the output from *lean-debug*\r\n```\r\n06:43:57.794 -- after-change-function\r\n06:43:57.794 -- before-text: \r\n06:43:57.794 -- after-text: i\r\n06:43:58.114 -- after-change-function\r\n06:43:58.114 -- before-text: \r\n06:43:58.114 -- after-text: m\r\n06:43:58.423 -- after-change-function\r\n06:43:58.423 -- before-text: \r\n06:43:58.423 -- after-text: p\r\n06:43:58.663 -- after-change-function\r\n06:43:58.663 -- before-text: \r\n06:43:58.663 -- after-text: o\r\n06:43:58.747 -- after-change-function\r\n06:43:58.747 -- before-text: \r\n06:43:58.747 -- after-text: r\r\n06:43:58.974 -- after-change-function\r\n06:43:58.974 -- before-text: \r\n06:43:58.974 -- after-text: t\r\n06:43:59.090 -- after-change-function\r\n06:43:59.090 -- before-text: \r\n06:43:59.090 -- after-text:  \r\n06:43:59.939 -- after-change-function\r\n06:43:59.939 -- before-text: \r\n06:43:59.939 -- after-text: t\r\n06:44:00.448 -- get-info-record-at-point: (INFO 1 nil)\r\n06:44:00.449 -- send-cmd-async: INFO 1\r\n06:44:00.449 -- send-cmd-async: queue len = 1\r\n06:44:00.449 -- send-cmd-async: REPLACE 1\r\n06:44:00.449 -- send-cmd-async: queue len = 1\r\n06:44:00.449 -- Sent Message:\r\nREPLACE 1\r\nimport t\r\n\r\n06:44:00.449 -- Sent Message:\r\nINFO 1\r\n\r\n06:44:00.450 -- send-cmd-async: added to INFO the queue, queue size = 2\r\n06:44:00.450 -- send-cmd-async: call handler\r\n06:44:00.450 -- set-timer-for-event-handler\r\n06:44:00.454 -- Received Message:\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n\r\n\r\n06:44:00.502 -- after-change-function\r\n06:44:00.502 -- before-text: t\r\n06:44:00.502 -- after-text: \r\n06:44:00.579 -- after-change-function\r\n06:44:00.579 -- before-text: \r\n06:44:00.579 -- after-text: d\r\n06:44:01.092 -- get-info-record-at-point: (INFO 1 nil)\r\n06:44:01.092 -- send-cmd-async: INFO 1\r\n06:44:01.092 -- send-cmd-async: queue len = 2\r\n06:44:01.092 -- send-cmd-async: REPLACE 1\r\n06:44:01.092 -- send-cmd-async: queue len = 2\r\n06:44:01.092 -- Sent Message:\r\nREPLACE 1\r\nimport d\r\n\r\n06:44:01.093 -- Sent Message:\r\nINFO 1\r\n\r\n06:44:01.093 -- send-cmd-async: added to INFO the queue, queue size = 3\r\n06:44:01.093 -- send-cmd-async: call handler\r\n06:44:01.093 -- set-timer-for-event-handler\r\n06:44:01.097 -- after-change-function\r\n06:44:01.097 -- before-text: \r\n06:44:01.097 -- after-text: a\r\n06:44:01.118 -- Received Message:\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n\r\n\r\n06:44:01.352 -- after-change-function\r\n06:44:01.352 -- before-text: \r\n06:44:01.352 -- after-text: t\r\n06:44:01.627 -- after-change-function\r\n06:44:01.627 -- before-text: \r\n06:44:01.627 -- after-text: a\r\n06:44:01.827 -- after-change-function\r\n06:44:01.827 -- before-text: \r\n06:44:01.827 -- after-text: .\r\n06:44:19.200 -- get-info-record-at-point: (INFO 1 nil)\r\n06:44:19.201 -- send-cmd-async: INFO 1\r\n06:44:19.201 -- send-cmd-async: queue len = 3\r\n06:44:19.201 -- send-cmd-async: REPLACE 1\r\n06:44:19.201 -- send-cmd-async: queue len = 3\r\n06:44:19.201 -- Sent Message:\r\nREPLACE 1\r\nimport data.\r\n\r\n06:44:19.201 -- Sent Message:\r\nINFO 1\r\n\r\n06:44:19.202 -- send-cmd-async: added to INFO the queue, queue size = 4\r\n06:44:19.202 -- send-cmd-async: call handler\r\n06:44:19.202 -- set-timer-for-event-handler\r\n06:44:19.204 -- Received Message:\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n\r\n\r\n06:44:19.308 -- The following pre-message will be thrown away:\r\n06:44:19.308 -- \r\n06:44:19.308 -- process-message-with-cont: type = INFO, cmd-type = INFO\r\n06:44:19.308 -- process-message-with-cont: body\r\n-----\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n-----\r\n\r\n06:44:19.308 -- Process: INFO\r\n06:44:19.308 -- executing continucation for get-info-record-at-point 0: NAY DETECTED\r\n06:44:19.308 -- event-handler: processed. now the queue size = 3\r\n\r\n06:44:19.308 -- set-timer-for-event-handler\r\n06:44:19.413 -- The following pre-message will be thrown away:\r\n06:44:19.413 -- \r\n\r\n06:44:19.413 -- process-message-with-cont: type = INFO, cmd-type = INFO\r\n06:44:19.413 -- process-message-with-cont: body\r\n-----\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n-----\r\n\r\n06:44:19.414 -- Process: INFO\r\n06:44:19.414 -- executing continucation for get-info-record-at-point 0: NAY DETECTED\r\n06:44:19.414 -- event-handler: processed. now the queue size = 2\r\n\r\n06:44:19.414 -- set-timer-for-event-handler\r\n06:44:19.515 -- The following pre-message will be thrown away:\r\n06:44:19.515 -- \r\n\r\n06:44:19.515 -- process-message-with-cont: type = INFO, cmd-type = INFO\r\n06:44:19.515 -- process-message-with-cont: body\r\n-----\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n-----\r\n\r\n06:44:19.515 -- Process: INFO\r\n06:44:19.515 -- executing continucation for get-info-record-at-point 0: NAY DETECTED\r\n06:44:19.515 -- event-handler: processed. now the queue size = 1\r\n\r\n06:44:19.515 -- set-timer-for-event-handler\r\n06:44:20.018 -- get-info-record-at-point: (INFO 1 nil)\r\n06:44:20.018 -- send-cmd-async: INFO 1\r\n06:44:20.018 -- send-cmd-async: queue len = 1\r\n06:44:20.018 -- Sent Message:\r\nINFO 1\r\n\r\n06:44:20.018 -- send-cmd-async: added to INFO the queue, queue size = 2\r\n06:44:20.019 -- send-cmd-async: call handler\r\n06:44:20.019 -- set-timer-for-event-handler\r\n06:44:20.020 -- Received Message:\r\n-- BEGININFO\r\n-- ENDINFO\r\n\r\n\r\n06:45:53.814 -- get-info-record-at-point: (INFO 1 nil)\r\n06:45:53.854 -- send-cmd-async: INFO 1\r\n06:45:53.854 -- send-cmd-async: queue len = 2\r\n06:45:53.855 -- Sent Message:\r\nINFO 1\r\n\r\n06:45:53.855 -- send-cmd-async: added to INFO the queue, queue size = 3\r\n06:45:53.855 -- send-cmd-async: call handler\r\n06:45:53.855 -- set-timer-for-event-handler\r\n06:45:53.856 -- Received Message:\r\n-- BEGININFO\r\n-- ENDINFO\r\n\r\n\r\n06:45:53.961 -- The following pre-message will be thrown away:\r\n06:45:53.961 -- \r\n\r\n06:45:53.961 -- process-message-with-cont: type = INFO, cmd-type = INFO\r\n06:45:53.961 -- process-message-with-cont: body\r\n-----\r\n-- BEGININFO STALE NAY\r\n-- ENDINFO\r\n-----\r\n\r\n06:45:53.961 -- Process: INFO\r\n06:45:53.962 -- executing continucation for get-info-record-at-point 0: NAY DETECTED\r\n06:45:53.962 -- event-handler: processed. now the queue size = 2\r\n\r\n06:45:53.962 -- set-timer-for-event-handler\r\n06:45:54.068 -- The following pre-message will be thrown away:\r\n06:45:54.068 -- \r\n\r\n06:45:54.068 -- process-message-with-cont: type = INFO, cmd-type = INFO\r\n06:45:54.068 -- process-message-with-cont: body\r\n-----\r\n-- BEGININFO\r\n-- ENDINFO\r\n-----\r\n\r\n06:45:54.068 -- Process: INFO\r\n06:45:54.069 -- executing continucation for get-info-record-at-point: OK\r\n06:45:54.069 -- event-handler: processed. now the queue size = 1\r\n\r\n06:45:54.069 -- set-timer-for-event-handler\r\n```"}}