Email Gateway (Aug 19 2022 at 14:46): Email Gateway (Aug 19 2022 at 14:46):From: Lars Noschinski <noschinl@in.tum.de>
Unfortunately, I do not have any experience in this area. It might be
worth skimming through Makarius' postings. He dropped some hints about
Scala/ML interaction over the time.
For terms in YXML format: As far as I understand, the standard
Isabelle(/ML) functions for parsing terms accept the "normal"
representation as well as the YXML representation; so one could just
generate theory files with the latter instead of the former (at expense
of human readability). There is this bit about it in the NEWS file:
* The inner syntax of sort/type/term/prop supports inlined YXML
representations within quoted string tokens. By encoding logical
entities via Term_XML (in ML or Scala) concrete syntax can be
bypassed, which is particularly useful for producing bits of text
under external program control.
So have a look at files at src/Pure/term_xml.{ML,scala} -- they describe
the XML representation of terms. YXML is just a (binary) representation
of (a subset of) XML. It should be described in either the
implementation or the system manual.
-- Lars
Last updated: Apr 23 2024 at 16:19 UTC