Re: GDB/MI Output syntax

[Andrew Cagney <cagney@gnu.org>]

>>>> >Andrew, were you suggesting something like this?
>>>> >
>>>> >from
>>>> >   output ==> ( out-of-band-record )* [ result-record ] "(gdb)" nl
>>>> >to
>>>> >   output ==> (out-of-band-record nl)* [ result-record nl] "(gdb)" nl
>>>> >
>>>> >and removing the 'nl' everywhere else?
>>
>>> 
>>> Yep.
>>> 
>>
>>>> >That might actually work. Although, I don't personally know a way of
>>>> >changing a grammar and guaranteeing that there the same.
>>
>>> 
>>> A series of rewrites where NL is slow pushed down should eventually 
>>> result in the old grammar (well except that it would be fixed).
> 
> 
> By the way you are talking, I can't tell if you are going to do this, or
> if you expect someone else to do it?

I eye balled it - it puts a NL at the end of each record which was the 
intent.

> Should I just post a new grammar with the suggestion? The problem is, I
> don't know how to prove that the new grammar is equivalant to the old
> grammar. Is there a way to do that?

Well, to be pedantic, the old grammer contained a bug which this fixes 
so we can't prove equivalence.  However using a sequence of 
transformations (rewrite was a poor choice of word) we can show rough 
equivalence.  For instance:

> @item @var{output} @expansion{}
> @code{( @var{out-of-band-record} @var{nl} )* [ @var{result-record} @var{nl} ] "(gdb)" @var{nl}}
> 
> @item @var{result-record} @expansion{}
> @code{[ @var{token} ] "^" @var{result-class} ( "," @var{result} )*}

Moving result-record's NL into the result-record production yields:

> @item @var{output} @expansion{}
> @code{( @var{out-of-band-record} @var{nl})* [ @var{result-record} ] "(gdb)" @var{nl}}
> 
> @item @var{result-record} @expansion{}
> @code{ [ @var{token} ] "^" @var{result-class} ( "," @var{result} )* @var{nl}}

which is the easy one done.  The other while longer and more tedious is 
similar except it ends up pushing an NL down into stream-record (where 
it was missing).

Is this what you ment?

Andrew