Re: [isabelle] detaching sml mode from Prover IDE
On Sat, 30 Aug 2014, Gergely Buday wrote:
first of all, thanks for the developers for the sml mode.
Note that the "sml mode" is a full-scale IDE.
In the narrow sense, there is an "sml mode" in terms of jEdit, but that is
just the token handler for syntax highlighting.
Would it be possible to detach the sml mode of the Prover IDE from
Isabelle? If one wants to develop in Standard ML, downloading the
whole Isabelle release is too much of a good thing.
Can you be more specific about the last sentence? The Isabelle
distribution is not exactly small, but I never heard any complaints about
it being too big. Rather, most people are glad that (almost) everything
is there by default and works without further ado.
There are three main parameters: download time/space, unpacking time, disk
space. Which one do you experience as a problem?
The Isabelle/SML IDE could be made a bit smaller than the default Isabelle
release, but not so much. I guess that 50% size reduction would be the
maximum, after considerable efforts.
Just for marketing reasons, a "big" IDE might be actually better, because
this is what users see from other IDEs as well.
An actual benefit might be a way to bypass the bulky Isabelle/HOL build
process, and just use Pure, but that requires again some more features to
select "installation options" on startup.
This archive was generated by a fusion of
Pipermail (Mailman edition) and