This functionality is to enable Tinker to display and edit term in the GUI side. See the following info from the isabelle mail list:
"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."
@ggrov
plebras
commented
9 years ago
This functionality is to enable Tinker to display and edit term in the GUI side. See the following info from the isabelle mail list:
"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." @ggrov