{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/289","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/289/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/289/comments","events_url":"https://api.github.com/repos/coq/coq/issues/289/events","html_url":"https://github.com/coq/coq/pull/289","id":179045450,"number":289,"title":"[notation] Allow to retrieve notations with defined printing rules.","user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars.githubusercontent.com/u/7192257?v=3","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2016-09-24T18:45:11Z","updated_at":"2016-09-26T12:24:03Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/289","html_url":"https://github.com/coq/coq/pull/289","diff_url":"https://github.com/coq/coq/pull/289.diff","patch_url":"https://github.com/coq/coq/pull/289.patch"},"body":"The ML side lacks a method to query Coq for notations with defined\r\nprinting rules. This commit adds a method\r\n`get_defined_printing_notations` to that purpose.\r\n(Suggestions on the naming welcome).\r\n\r\nThis is very useful for instance in SerAPI. However, note that I believe\r\nthat in the medium-term, the `Notation` interface needs a bit of\r\nrefactoring to allow programmatic access and manipulation of notations."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/249555190","html_url":"https://github.com/coq/coq/pull/289#issuecomment-249555190","issue_url":"https://api.github.com/repos/coq/coq/issues/289","id":249555190,"user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars.githubusercontent.com/u/460771?v=3","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"created_at":"2016-09-26T12:24:03Z","updated_at":"2016-09-26T12:24:03Z","body":"How do you see this? \r\n\r\nTo have it controlled by the UI user, e.g. to have each notation clickable and the UI user being able to dynamically define a new printing, for this session, or for the next sessions too, remembering them in a preference file? Or a configuration panel telling how to map notation keys to alternative output, say mapping `\"_ * _\"` to `\"_ × _\"`?\r\n\r\nOr to let it be controlled by the Coq file developer, using e.g. the alternative `format` field which supports to write say e.g. `format \"latex\" \"x \\times y\"` or `format \"utf8\" \"x × y\"`, or `format \"pg\" \"x × y\"`, or `format \"html\" \"<div> x &times; y </div>\"`, etc?\r\n\r\nOr, maybe both? Using by default the format given in the Coq file but letting it be locally modified by the UI user?\r\n\r\n"}}
{"actor":{"display_login":"herbelin"}}