Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] libisabelle: embedding on Java-side: terms (Ma...


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC