I had a student project writing a SCRIPT tag interpreter for PolyML as a firefox add-on: https://addons.mozilla.org/en-US/firefox/addon/polychrome/ (PolyChrome)
This let you do some HTML-based UI.
I actually think that HTML5, especially Polymer, provides a pretty good way to write cross-platform UI.
It's interesting to consider what the best way to give some kind of access to that for ML is. I'm not convinced that our approach in PolyChrome is the best on reflection, but it was fun to see ML running in web-pages.
best, lucas
On 12 December 2014 at 05:17, Makarius <makarius at sketis.net> wrote:
On Fri, 12 Dec 2014, me at beroal.in.ua wrote:
<offtopic>IMHO, Web GUI is a fad. HTML was not intended for GUI, and this
poor creature continues to be, not quite fit for what it is used, a pile of amendments without much thought. It surely has its advantages, network capability and no installation, but the main one is popularity or hype.</offtopic>
I don't think it is totally off-topic. ML/SML started out in the interactive theorem proving community (as the "meta-language" of the LCF prover). The question behind the GUI is how to connect ML (and thus the proof assistant) to the outside world: both end-users and other systems.
I've found my own answers for that with the PIDE framework, which is a bi-ped with Scala and ML. Thus the connectivity happens on the JVM world, using whatever is there. For Isabelle/PIDE/jEdit I use the AWT/Swing GUI framework, which sort of works out, although it is not ideal. It is difficult to find fundamentally better GUI frameworks, though, and the main requirement is a proper editor on top of the GUI framework. The resulting system of Isabelle/jEdit is then a traditional (old-fashioned!) rich-client IDE application.
HTML (4 or 5) + X connectivity has always been there as an alternative. Some people have investigated that to some extent and with some success: both for Scala and Poly/ML, e.g. Isabelle/CLIDE from the Bremen guys.
After so many years pondering local GUI vs. remote HTTP / local HTML front-ends, my impression is that neither is a really good solution. Something fundamental needs to change in computing technology to get really good solutions. We have to make the best out of the things we see today, and extrapolate to a better future.
Back to the original question: a public version of the aforementioned GTK C bindings for Poly/ML would be great. Although GTK is just one of the many legacy GUI frameworks in use. Qt4 might do a better job, but I can't say anything myself, apart from pointing to some core Linux guys (Dirk Hohndel and Linus Torvalds) who moved from GTK to Qt4 recently, see https://www.youtube.com/watch?v=ON0A1dsQOV0
Makarius
http://stop-ttip.org 1,139,504 people so far
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml