Spark Editors?

Spark Editors?

[Diogenes]

Besides GPS, what other text editors and/or IDEs are out there that at least support Spark syntax highlighting?

I prefer something lightweight. GPS is nice, but it's a little too much for my work flow.

I prefer things like Sublime Text, Nedit, or even VIM.

Any pointers?

Diogenes

Re: Spark Editors?

[Paul Rubin]

Diogenes <phathax0r@gmail.com> writes:
> Besides GPS, what other text editors and/or IDEs are out there that at
> least support Spark syntax highlighting?

Emacs has an Ada mode.  Does Spark require much more than that?  I
thought Spark was a subset of Ada.

Re: Spark Editors?

[Simon Wright]

Paul Rubin <no.email@nospam.invalid> writes:

> Diogenes <phathax0r@gmail.com> writes:
>> Besides GPS, what other text editors and/or IDEs are out there that at
>> least support Spark syntax highlighting?
>
> Emacs has an Ada mode.  Does Spark require much more than that?  I
> thought Spark was a subset of Ada.

Pre-2014 SPARK used comments with a special syntax. I believe there is
an Emacs mode for that. Why you'd want to use pre-2014 SPARK if you
could help it I don't know.

Re: Spark Editors?

[Stephen Leake]

On Saturday, October 8, 2016 at 2:40:54 PM UTC-5, Paul Rubin wrote:
> Diogenes <> writes:
> > Besides GPS, what other text editors and/or IDEs are out there that at
> > least support Spark syntax highlighting?
> 
> Emacs has an Ada mode.  Does Spark require much more than that?  I
> thought Spark was a subset of Ada.

As implemented in recent GNAT versions, SPARK is a set of attributes on Ada types and subprograms, and a set of restrictions. So it is strictly a subset of Ada 2015, yes.

Emacs Ada mode 5.2.0, available from GNU ELPA (install via list-packages) supports attributes.

Most people would not class Emacs as "lightweight", but it is far more customizable than GPS, so you can make it support your workflow precisely.

There are other files that SPARK uses, for proofs. I haven't used SPARK, so I'm not familiar with their syntax. Does GPS provide syntax highlighting for them?

GPS also provides support for running SPARK and displaying the results. In Emacs, that would be done by a Makefile and the Emacs compilation error mechanism. I don't know if that is sufficient.