On Thu, 2 Oct 2014, Tjark Weber wrote:
1. I suspect that the ITP aspect of Isabelle may put off people who
just want to write SML code. (For instance, there are many documents
and panels visible in the UI that are entirely irrelevant to SML
programming.) If you had unlimited time, I would suggest that the SML
IDE be released separately from Isabelle.
This is only the first release of the SML PIDE, but I have started
thinking about these questions before. It is probably mainly a matter to
re-package the system such that it looks more like an SML IDE outright.
Many things are possible, but it also requires some work. Does anybody
has smart ideas to find some funding for such projects? It might be also
interesting for David Matthews himself, to provide even more IDE support
at the bottom, e.g. inclusion of the debugger.
We also need to find out how many people are still there to use SML. So
far there are already 9 supporters on
http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-or-linux-or-mac
and the green tick has changed as well :-)
2. The need to have a theory file (no matter how simple) is slightly
unfortunate. Would an Isabelle/jEdit option "-sml" (or similar) be
feasible to make the enclosing theory redundant, at least for
single-file SML projects?
"Unfortunate" (like "fix") is a word of this odd street language that has
emerged in recent years and is better ignored. The enclosing theory file
is like a project file, but with slightly odd syntax for that purpose,
although not too bad compared to the traditional "use" script.
There might be other ways emerging to assemble ML files; or maybe just
some IDE support to generate such templates.
There was also a private discussion with Larry Paulson, to re-use the
model of the SML/NJ compilation management, whatever that might be
exactly -- we still need to find out.
3. I noticed that "use" is not available, and that "print" doesn't
affect the output panel. A document that summarizes such differences
(and explains, e.g., how to perform I/O instead) might be useful.
Note that "use" is not part of Standard ML. This touches again the
question how SML projects are actually managed. For the IDE to work, the
control over the ML files needs to be given to the IDE, not the ML
program.
Further note that "print" is also not Standard ML, although TextIO.print
is covered by the Basis Library. That raw stateful output is in conflict
with the stateless model of PIDE, but it works as specified: via stdout,
which is shown in PIDE in the Raw Output panel. In contrast, the
Documentation panel includes src/Tools/SML/Examples.thy with some examples
to re-use stateless Isabelle output in SML.
4. Ctrl+click on certain built-in operators, such as *, takes me to an
empty buffer called "Standard Basis". Surely some explanatory message
could be displayed in the buffer.
This information is produced by Poly/ML at the very bottom. E.g. the
"length" function refers to $ML_SOURCE/basis/List.sml as expected.
David Matthews might be able to tell what happens with * (or +). I know
myself from Isabelle/Pure bootstrapping, that formal references to very
basic things are sometimes surprising, by construction of the initial
environment.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
