From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.129.137.6 with SMTP id z6mr7515198ywf.122.1476025492468;
        Sun, 09 Oct 2016 08:04:52 -0700 (PDT)
X-Received: by 10.157.11.146 with SMTP id 18mr2668287oth.13.1476025492381;
 Sun, 09 Oct 2016 08:04:52 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!g45no1066159qte.1!news-out.google.com!203ni4749itk.0!nntp.google.com!l13no1587895itl.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sun, 9 Oct 2016 08:04:52 -0700 (PDT)
In-Reply-To: <87shs6vdbu.fsf@nightsong.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=76.218.37.33;
 posting-account=W2gdXQoAAADxIuhBWhPFjUps3wUp4RhQ
NNTP-Posting-Host: 76.218.37.33
References: <5ddfd78e-83e3-40f6-b9c1-ad7bf40ac228@googlegroups.com>
 <87shs6vdbu.fsf@nightsong.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <05ffa817-0412-4117-842d-bd1e0ef1e748@googlegroups.com>
Subject: Re: Spark Editors?
From: Stephen Leake <stephen_leake@stephe-leake.org>
Injection-Date: Sun, 09 Oct 2016 15:04:52 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:32061
Date: 2016-10-09T08:04:52-07:00
List-Id: <comp.lang.ada>

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.