{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/67","labels_url":"https://api.github.com/repos/coq/coq/issues/67/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/67/comments","events_url":"https://api.github.com/repos/coq/coq/issues/67/events","html_url":"https://github.com/coq/coq/pull/67","id":89535168,"number":67,"title":"Add a [Show Proof.] query to CoqIDE.","user":{"login":"cmangin","id":2060299,"avatar_url":"https://avatars.githubusercontent.com/u/2060299?v=3","gravatar_id":"","url":"https://api.github.com/users/cmangin","html_url":"https://github.com/cmangin","followers_url":"https://api.github.com/users/cmangin/followers","following_url":"https://api.github.com/users/cmangin/following{/other_user}","gists_url":"https://api.github.com/users/cmangin/gists{/gist_id}","starred_url":"https://api.github.com/users/cmangin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cmangin/subscriptions","organizations_url":"https://api.github.com/users/cmangin/orgs","repos_url":"https://api.github.com/users/cmangin/repos","events_url":"https://api.github.com/users/cmangin/events{/privacy}","received_events_url":"https://api.github.com/users/cmangin/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-06-19T11:00:56Z","updated_at":"2015-07-01T19:11:50Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/67","html_url":"https://github.com/coq/coq/pull/67","diff_url":"https://github.com/coq/coq/pull/67.diff","patch_url":"https://github.com/coq/coq/pull/67.patch"},"body":"I find myself typing \"Show Proof.\" a lot sometimes, and was wondering why there wasn't a shortcut for that. Maybe there is a reason?\r\nAnyway, if there is none, here is a patch that adds this."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/117798119","html_url":"https://github.com/coq/coq/pull/67#issuecomment-117798119","issue_url":"https://api.github.com/repos/coq/coq/issues/67","id":117798119,"user":{"login":"gares","id":1013846,"avatar_url":"https://avatars.githubusercontent.com/u/1013846?v=3","gravatar_id":"","url":"https://api.github.com/users/gares","html_url":"https://github.com/gares","followers_url":"https://api.github.com/users/gares/followers","following_url":"https://api.github.com/users/gares/following{/other_user}","gists_url":"https://api.github.com/users/gares/gists{/gist_id}","starred_url":"https://api.github.com/users/gares/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gares/subscriptions","organizations_url":"https://api.github.com/users/gares/orgs","repos_url":"https://api.github.com/users/gares/repos","events_url":"https://api.github.com/users/gares/events{/privacy}","received_events_url":"https://api.github.com/users/gares/received_events","type":"User","site_admin":false},"created_at":"2015-07-01T19:11:50Z","updated_at":"2015-07-01T19:11:50Z","body":"What do you mean by half?  The template menu is already too huge.  The query one is indeed short. To my understanding what @cmangin was asking for is a key binding for Show Proof, not just an entry in one of the drop down menus.\r\n\r\nIIRC, F1+RETURN should pretty much behave as \"run last query\".  If not, we could add a shortcut for that as a sort of \"meta shortcut\" for the favorite, non already key-bound, query of any user.\r\nAlternatively, we could add a \"automatically run checkbox\" in the query pane/tab so that you can detach it, and see it being automatically updated every time the goal window is.\r\nI'm just brainstorming here, but I'd rather avoid having a shortcut reserved for each query, since their frequency seems to be pretty personal.  E.g. I never, ever, do Show Proof... the proof I want to see is the text in the text buffer, not the lambda term; ditto for people using a lot of Ltac automation; but I guess it is the converse for HoTT people, since their proofs are transparent, or you and cmagin.  BTW, why do you need to look at the proof term?"}}