Re: json objects in jStar

[Radu Grigore]

On Tue, Sep 28, 2010 at 4:46 PM, D. Aleknaviciute <da...@cam.ac.uk> wrote:
> Since the delimiters are "json" at the beginning and "new line" at
> the end, your [newlines do] not work with Eclipse.
>
> Do we really want to show json object as an output in console?

Sorry for making those changes without testing. What do I need to do
to get install/use the Eclipse plugin?

I added newlines to make it easier for whoever debugs jStar, not
because I thought that users will see it.

Did you consider adding location information to jStar's normal
messages and parsing those? For example, gcc uses the format
"^FILENAME:LOCATION: MESSAGE$. That way there's no need for a '-e'
options, and there's no need to maintain two output formats for error
messages.

regards,
radu