{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/fstar-mode.el/issues/50","repository_url":"https://api.github.com/repos/FStarLang/fstar-mode.el","labels_url":"https://api.github.com/repos/FStarLang/fstar-mode.el/issues/50/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/fstar-mode.el/issues/50/comments","events_url":"https://api.github.com/repos/FStarLang/fstar-mode.el/issues/50/events","html_url":"https://github.com/FStarLang/fstar-mode.el/issues/50","id":215541307,"number":50,"title":"Supporting #info requests","user":{"login":"nikswamy","id":6163359,"avatar_url":"https://avatars3.githubusercontent.com/u/6163359?v=3","gravatar_id":"","url":"https://api.github.com/users/nikswamy","html_url":"https://github.com/nikswamy","followers_url":"https://api.github.com/users/nikswamy/followers","following_url":"https://api.github.com/users/nikswamy/following{/other_user}","gists_url":"https://api.github.com/users/nikswamy/gists{/gist_id}","starred_url":"https://api.github.com/users/nikswamy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikswamy/subscriptions","organizations_url":"https://api.github.com/users/nikswamy/orgs","repos_url":"https://api.github.com/users/nikswamy/repos","events_url":"https://api.github.com/users/nikswamy/events{/privacy}","received_events_url":"https://api.github.com/users/nikswamy/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2017-03-20T20:13:19Z","updated_at":"2017-03-21T16:25:06Z","closed_at":null,"body":"Hi Clement, \r\n\r\nThe latest master version of F* now supports a new feature that I would like to make available from fstar-mode.el. \r\n\r\nIn response to an \"#info filename row col\" request, `fstar --in` will reply with either\r\n\r\n ```<info> identifier : type (defined at filename:(row, col))</info>```\r\n\r\nOr \r\n\r\n```No information found at filename:(row, col)```\r\n\r\nI'm hoping to provide a feature where the user hovers the mouse over an identifier in the current buffer and fstar-mode.el floats the information returned by fstar for that identifier, if any.\r\n\r\nIdeally, through some other option, it would be possible also jump to the source location that defines this identifier. \r\n\r\nIf there are any easy hints you can provide about how to implement this functionality in fstar-mode.el (or thoughts about how to improve my proposed design) that would be most helpful! \r\n\r\nThanks!\r\n-Nik\r\n\r\nPS: Thanks to @leodemoura for suggesting some of this.\r\n"},"comment":{"url":"https://api.github.com/repos/FStarLang/fstar-mode.el/issues/comments/288134607","html_url":"https://github.com/FStarLang/fstar-mode.el/issues/50#issuecomment-288134607","issue_url":"https://api.github.com/repos/FStarLang/fstar-mode.el/issues/50","id":288134607,"user":{"login":"nikswamy","id":6163359,"avatar_url":"https://avatars3.githubusercontent.com/u/6163359?v=3","gravatar_id":"","url":"https://api.github.com/users/nikswamy","html_url":"https://github.com/nikswamy","followers_url":"https://api.github.com/users/nikswamy/followers","following_url":"https://api.github.com/users/nikswamy/following{/other_user}","gists_url":"https://api.github.com/users/nikswamy/gists{/gist_id}","starred_url":"https://api.github.com/users/nikswamy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikswamy/subscriptions","organizations_url":"https://api.github.com/users/nikswamy/orgs","repos_url":"https://api.github.com/users/nikswamy/repos","events_url":"https://api.github.com/users/nikswamy/events{/privacy}","received_events_url":"https://api.github.com/users/nikswamy/received_events","type":"User","site_admin":false},"created_at":"2017-03-21T16:25:06Z","updated_at":"2017-03-21T16:25:06Z","body":"Hi Clement, \r\n\r\nAbout saving a file:\r\nThe current buffer does not have to be saved. It's a request for information about either (a) the current buffer (which need not be saved) or (b) any saved file in the the current buffer's dependence graph. The user interface I propose doesn't make it particularly easy to make a query in class (b). However, I could imagine a scenario where on starts in the current buffer, jumps to a definition in another file, and asks F* for information about some symbol in that file.\r\n\r\nAbout #info-name: I'm not sure what scope one would use to resolve the name. Any suggestions?\r\n\r\nAbout (a)synchrony: The command I'm proposing is synchronous. But, an async variant is clearly more useful. However, that would require some re-architecting of `fstar --in`\r\n\r\nAbout size of types: Current they can be very large if printed in full detail. However, I would expect this info request to, by default, print only \"lax\" types, which are smaller (e.g., usually less than a line but sometimes up to 10 lines in source formatting---see, for example, https://github.com/FStarLang/FStar/blob/master/examples/low-level/crypto/Crypto.AEAD.Decrypt.fst#L83 up to line 92). We would also  allow the user to ratchet up detail based on verbosity options already available using the #set-options directive in an F\\* file. Also, @kyod, @qunyanm  and others are working on better pretty printers fro F\\* terms, so this should keep improving.\r\n\r\nAbout implementation:\r\n\r\nThanks for the tips. Totally understand that you're busy with other stuff. These tips may already be enough to get me started ... I should dig into the code of fstar-mode.el anyway.\r\n\r\nThe latest master version of F* supports this feature. However, it has not been tested much yet ... I was expecting to do that as part of editor integration."}}
{"actor":{"display_login":"nikswamy"}}