{"action":"created","issue":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/363","repository_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL","labels_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/363/labels{/name}","comments_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/363/comments","events_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/363/events","html_url":"https://github.com/HOL-Theorem-Prover/HOL/issues/363","id":179681732,"number":363,"title":"Remove ProvideUnicode module and Unicode trace","user":{"login":"mn200","id":145647,"avatar_url":"https://avatars1.githubusercontent.com/u/145647?v=4","gravatar_id":"","url":"https://api.github.com/users/mn200","html_url":"https://github.com/mn200","followers_url":"https://api.github.com/users/mn200/followers","following_url":"https://api.github.com/users/mn200/following{/other_user}","gists_url":"https://api.github.com/users/mn200/gists{/gist_id}","starred_url":"https://api.github.com/users/mn200/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mn200/subscriptions","organizations_url":"https://api.github.com/users/mn200/orgs","repos_url":"https://api.github.com/users/mn200/repos","events_url":"https://api.github.com/users/mn200/events{/privacy}","received_events_url":"https://api.github.com/users/mn200/received_events","type":"User","site_admin":false},"labels":[{"id":162624,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/labels/Feature%20Request","name":"Feature Request","color":"0b02e1","default":false},{"id":149312,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/labels/Printing-Parsing","name":"Printing-Parsing","color":"02d7e1","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-09-28T05:15:48Z","updated_at":"2017-08-02T03:58:53Z","closed_at":null,"body":"This functionality adds a lot of complexity to the parsing code and doesn't provide much more in practice than the `PP.avoid_unicode` trace.  To be precise, turning the `Unicode` trace off prevents Unicode syntax from parsing, and prevents Unicode characters from appearing when terms are printed. The `PP.avoid_unicode` trace stops the latter, but still allows parsing of Unicode syntax. My feeling is that this is probably preferable and that removing the possibility of getting the `Unicode` trace's behaviour will be no great loss. \n## <bountysource-plugin>\n\nWant to back this issue? **[Post a bounty on it!](https://www.bountysource.com/issues/38732996-remove-provideunicode-module-and-unicode-trace?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github)** We accept bounties via [Bountysource](https://www.bountysource.com/?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github).\n</bountysource-plugin>\n"},"comment":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/comments/319560951","html_url":"https://github.com/HOL-Theorem-Prover/HOL/issues/363#issuecomment-319560951","issue_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/363","id":319560951,"user":{"login":"mn200","id":145647,"avatar_url":"https://avatars1.githubusercontent.com/u/145647?v=4","gravatar_id":"","url":"https://api.github.com/users/mn200","html_url":"https://github.com/mn200","followers_url":"https://api.github.com/users/mn200/followers","following_url":"https://api.github.com/users/mn200/following{/other_user}","gists_url":"https://api.github.com/users/mn200/gists{/gist_id}","starred_url":"https://api.github.com/users/mn200/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mn200/subscriptions","organizations_url":"https://api.github.com/users/mn200/orgs","repos_url":"https://api.github.com/users/mn200/repos","events_url":"https://api.github.com/users/mn200/events{/privacy}","received_events_url":"https://api.github.com/users/mn200/received_events","type":"User","site_admin":false},"created_at":"2017-08-02T03:58:53Z","updated_at":"2017-08-02T03:58:53Z","body":"The infrastructure around `ProvideUnicode` currently causes the following unfortunate printing behaviour when the `Unicode` trace is true:\r\n```` \r\n> ``UNIV 3``;\r\nval it = “𝕌 ARB 3”: term\r\n````\r\nwhile it might be possible to mess further with `ProvideUnicode` this seems more like a reason to just get rid of it."}}
{"actor":{"display_login":"mn200"}}