{"action":"created","issue":{"url":"https://api.github.com/repos/ggrov/tinker/issues/1","labels_url":"https://api.github.com/repos/ggrov/tinker/issues/1/labels{/name}","comments_url":"https://api.github.com/repos/ggrov/tinker/issues/1/comments","events_url":"https://api.github.com/repos/ggrov/tinker/issues/1/events","html_url":"https://github.com/ggrov/tinker/issues/1","id":34067995,"number":1,"title":"import / export Isabelle term to Tinker GUI","user":{"login":"lyhlbyl","id":3641942,"avatar_url":"https://avatars.githubusercontent.com/u/3641942?v=3","gravatar_id":"","url":"https://api.github.com/users/lyhlbyl","html_url":"https://github.com/lyhlbyl","followers_url":"https://api.github.com/users/lyhlbyl/followers","following_url":"https://api.github.com/users/lyhlbyl/following{/other_user}","gists_url":"https://api.github.com/users/lyhlbyl/gists{/gist_id}","starred_url":"https://api.github.com/users/lyhlbyl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lyhlbyl/subscriptions","organizations_url":"https://api.github.com/users/lyhlbyl/orgs","repos_url":"https://api.github.com/users/lyhlbyl/repos","events_url":"https://api.github.com/users/lyhlbyl/events{/privacy}","received_events_url":"https://api.github.com/users/lyhlbyl/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/ggrov/tinker/labels/Tinker%20GUI","name":"Tinker GUI","color":"d4c5f9"},{"url":"https://api.github.com/repos/ggrov/tinker/labels/TODO","name":"TODO","color":"006b75"}],"state":"closed","locked":false,"assignee":{"login":"lyhlbyl","id":3641942,"avatar_url":"https://avatars.githubusercontent.com/u/3641942?v=3","gravatar_id":"","url":"https://api.github.com/users/lyhlbyl","html_url":"https://github.com/lyhlbyl","followers_url":"https://api.github.com/users/lyhlbyl/followers","following_url":"https://api.github.com/users/lyhlbyl/following{/other_user}","gists_url":"https://api.github.com/users/lyhlbyl/gists{/gist_id}","starred_url":"https://api.github.com/users/lyhlbyl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lyhlbyl/subscriptions","organizations_url":"https://api.github.com/users/lyhlbyl/orgs","repos_url":"https://api.github.com/users/lyhlbyl/repos","events_url":"https://api.github.com/users/lyhlbyl/events{/privacy}","received_events_url":"https://api.github.com/users/lyhlbyl/received_events","type":"User","site_admin":false},"milestone":null,"comments":1,"created_at":"2014-05-22T10:13:22Z","updated_at":"2015-06-05T10:24:31Z","closed_at":"2015-06-05T10:24:31Z","body":"This functionality is to enable Tinker to display and edit term in the GUI side. See the following info from the isabelle mail list:\r\n\r\n\"by emitting an XML or YXML encoding of the format defined in $ISABELLE_HOME/src/Pure/term_xml.ML See also https://bitbucket.org/makarius/yxml to get some idea how this works, independently of the huge Isabelle code base.\"\r\n@ggrov "},"comment":{"url":"https://api.github.com/repos/ggrov/tinker/issues/comments/109252048","html_url":"https://github.com/ggrov/tinker/issues/1#issuecomment-109252048","issue_url":"https://api.github.com/repos/ggrov/tinker/issues/1","id":109252048,"user":{"login":"plebras","id":7670356,"avatar_url":"https://avatars.githubusercontent.com/u/7670356?v=3","gravatar_id":"","url":"https://api.github.com/users/plebras","html_url":"https://github.com/plebras","followers_url":"https://api.github.com/users/plebras/followers","following_url":"https://api.github.com/users/plebras/following{/other_user}","gists_url":"https://api.github.com/users/plebras/gists{/gist_id}","starred_url":"https://api.github.com/users/plebras/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/plebras/subscriptions","organizations_url":"https://api.github.com/users/plebras/orgs","repos_url":"https://api.github.com/users/plebras/repos","events_url":"https://api.github.com/users/plebras/events{/privacy}","received_events_url":"https://api.github.com/users/plebras/received_events","type":"User","site_admin":false},"created_at":"2015-06-05T10:24:31Z","updated_at":"2015-06-05T10:24:31Z","body":"see #45 "}}