> You have something like that in Coq/ex/indent.v.
> I dream of a smie with two grammars (and lexers): one for first lines of
> commands and one inside commands. It would greatly simplify things I think.
I don't really know how to define "first lines" and "inside", but you
can definitely have
On 03/12/2018 12.15, Emilio Jesús Gallego Arias wrote:
> Emilio Jesús Gallego Arias writes:
>
>> - Isabelle / PIDE understands complete projects;
>> - reliable async support and integration with external tools;
>> - better error reporting and handling.
>
> Some more: on the fly checking, real
Emilio Jesús Gallego Arias writes:
> - Isabelle / PIDE understands complete projects;
> - reliable async support and integration with external tools;
> - better error reporting and handling.
Some more: on the fly checking, real completion, semantic folding; I'm
sure experienced Isabelle users
On 03/12/2018 11.57, Emilio Jesús Gallego Arias wrote:
> In the first case, my opinion (and the one of quite a few of my
> colleagues) is yes, clearly ahead.
But can you give concrete examples of extra features that they have?
And, re the coupling, are these worth being stuck with a single
Le lun. 3 déc. 2018 à 13:11, Emilio Jesús Gallego Arias a écrit
:
>
> I feel like this may be the moment to make it a bit more "stable".
Good news!
> However, I would expect adding PG support to SerAPI to require at least
> one or two Coq releases where it would be marked "experimental" and
