On Tue, 9 Dec 2014 00:02:24 +0100 (CET), Richard Molitor <gattschardo at googlemail.com> wrote:

Richard> So you might want to try just wrapping relevant parts of Richard> e.g. Gtk yourself and see how far you can get (don't know how Richard> wrapping C++ for getting Qt would work)

There was a project for a GTK wrapper discussed here not so long ago [1]

Personally I start to feel that UI tookits of this kind may be a dead end, and Web interfaces may be the only solution. If only that didn't require learning Javascript :-(

[1] http://thread.gmane.org/gmane.comp.lang.ml.polyml.general/501/focus=513

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 ----------------------------------------------------------------------------

On Fri, 12 Dec 2014 06:25:06 -0800, Lucas Dixon <lucas.dixon at gmail.com> wrote:

Lucas> I had a student project writing a SCRIPT tag interpreter for Lucas> PolyML as a firefox add-on: Lucas> https://addons.mozilla.org/en-US/firefox/addon/polychrome/ Lucas> (PolyChrome)

I tried to add the polychrome extension to my Iceweasel. The install is accepted, but there's no parrot icon. I think this is because of (or at least related to) the new interface in Firefox/Iceweasel itself after version 30 or so; there is no "status bar" anymore and hence also no special place for extension icons, my other extensions seem to place their icon in the huge "burger menu" on the right.

I didn't really expect it to work, but maybe I expected it to stop me at install time with a version check :-/

Do you know if this is supposed to work?

12/12/14 18:15, Ian Zimmerman wrote:

On Fri, 12 Dec 2014 14:17:27 +0100 (CET), Makarius <makarius at sketis.net> wrote:

Makarius> Back to the original question: a public version of the Makarius> aforementioned GTK C bindings for Poly/ML would be great.

Agreed, so could someone ping Phil Clayton about it? I am too shy (having been given access to an early version privately, and not having done anything with it).

Thanks for mentioning this Ian. Unfortunately I've only just caught up with this discussion.

GTK+ bindings do exist for Poly/ML as part of Giraffe Library, which I am developing. See below for a brief overview. The same bindings are also provided for MLton, allowing the same application code to compile with either compiler.

Giraffe Library is not publicly available yet because there are a couple of little loose ends that I want to tie up. However, I would be very happy to provide a copy to anyone wanting to try it out and feedback would be welcome. Giraffe Library is LGPL simply to have the same licence as GTK+ and company.

There are quite a few omissions in the library. Despite this, a lot can be done. To get a flavour of things, the ubiquitous Hello World example from the GTK+ tutorial is attached!

Regards, Phil

--------------- 1. Overview ---------------

Giraffe Library is a Standard ML library that provides an interface to GObject-based libraries, such as GTK+. The interface introduces some abstraction of the libraries to provide expected features of Standard ML such as:

- automatic memory management (garbage collection) - type-safety - no uninitialized values - portable source code

For the most part, Giraffe Library is generated automatically from the GIR data of the libraries. At present, interfaces to parts of the following libraries are available:

- GTK+ - Pango - GtkSourceView - VTE (Virtual Terminal Emulator)