Email Gateway (Aug 22 2022 at 11:07): Email Gateway (Aug 22 2022 at 11:07):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
I see the two files "term_xml.scala" and "term_xml.ML" [1], which seem
as elegant as many other files in Isabelle.
However, I did not yet start to study them, because I expect (from lots
of similar experiences) considerable efforts to comprehend the details ---
--- so I'd be very grateful If you would spend a minute from your
precious time!
Walther
PS: We consider to translate terms' XML.Trees into MathML content
format, most likely coding in Scala.
[1]
http://isabelle.in.tum.de/testboard/Isabelle/file/4050b243fc60/src/Pure/term_xml.ML
http://isabelle.in.tum.de/testboard/Isabelle/file/4050b243fc60/src/Pure/term_xml.scala
Email Gateway (Aug 22 2022 at 11:07):From: Walther Neuper <wneuper@ist.tugraz.at>
On 2015-08-12 10:15, Walther Neuper wrote:
Hi Lars,
(2) Could you, please, include an example in libisabelle, where you
ship
a lambda-term through PIDE/xml in both directions ?
What exactly do you mean here? An Isabelle term? Or are you talking
about an ML or a Scala function?
I mean an Isabelle term, which is not too simple.
I see the two files "term_xml.scala" and "term_xml.ML" [1], which seem
as elegant as many other files in Isabelle.However, I did not yet start to study them, because I expect (from
lots of similar experiences) considerable efforts to comprehend the
details ------ so I'd be very grateful If you would spend a minute from your
precious time!Walther
PS: We consider to translate terms' XML.Trees into MathML content
format, most likely coding in Scala.[1]
http://isabelle.in.tum.de/testboard/Isabelle/file/4050b243fc60/src/Pure/term_xml.ML
http://isabelle.in.tum.de/testboard/Isabelle/file/4050b243fc60/src/Pure/term_xml.scala
Last updated: Nov 21 2024 at 12:39 UTC