Does Lueng's RegExp library work with Isabelle/ML? Is there another regex lib devs use for Isabelle/ML?

Question

Q1: Does anyone know if Lueng's RegExp library works by magic with Isabelle/ML?

Q2: Is there some standard regex library that developers use for Isabelle/ML?

I had big plans to learn Scala, where my main application was going to be processing a THY to generate a TEX file.

I love the idea of Scala, but everyday, after thinking about how great it is, I have zero motivation to learn it, since learning about its full power will involve months of work, and then some ongoing study. My goal isn't to study programming, but to study mathematics with Isabelle.

So, I'm making a big switch to Isabelle/ML, because then the months of learning ML, and the ongoing study of it, will become a huge tool I can use for Isabelle proofs, and low-level setup of things like syntax.

The reason I didn't pick ML to begin with is because it doesn't have all the benefits of Scala for scripting, but I should be able to make ML work.

There is one huge worry, though, and that's ensuring I have a regular expression library to use. If I don't have regular expressions, it's a no-go.

On the page for the RegExp library above it says this on the web page:

All code in this section runs in the latest working version of Standard ML of New Jersey.

I don't know if that's a good sign, or a bad sign. At this point knowing simple things about Isabelle/ML are hard, other than there's those magnificent ML{*...*} and ML "..." commands I can use in a THY, and the comments about ML support I've been seeing for the next release of the PIDE.

In so many days, which might be weeks, I'll figure out all this for myself, but if someone can tell me now if does work, I can stop worrying.

Many people will know this, but there is the Isabelle Programming Tutorial by Christian Urban, with contributions from others. Knowing what's in there will be great.

Answer 1

That is a library for Standard ML of New Jersey, which has "Standard ML" in its name, but many non-standard add-ons, like the compilation manager CM.

I don't think it is worth spending too much time on that for Isabelle/ML. E.g. the parser combinators (structure Scan) are slightly more general and more functional in style.

Answer 2

I took a look at this too, and it appears to use non-standard Array libraries (from SML/NJ rather than the Basic Libraries). The conversion would probably be quite simple however.