On 13 Dec 2014, at 11:04, David Topham <dtopham at gmail.com> wrote:
I could use existing C/C++ GUI frameworks and have the logic of the program be in ML, but that means calling ML functions from C. Can that be done?
I?d humbly suggest you do something like this. Breaking your program along MVC lines (or X11 client/server if you prefer) makes it more robust to changes in UI technology. Makarius?s efforts with jEdit are at least the third mainstream interface that Isabelle has had.
The online documentation for the Poly/ML FFI (foreign function interface) is stale - as you can sort-of infer from the 1994 near the top.
If you read the CINTERFACE.ML file and/or CInterfaceSig.ML you will find all sorts of wonderful things. You want the ?toCfunction? value. This and the rest of the source code that I?ve seen is quite readable, though it might take some experimentation to get your head around how the API is supposed to be used. The old docs are helpful with that.
cheers peter