new hyps not proposed for completion when in diff mode.

[Matafou]

Hi
When a new tactic appear, it gets surreounded byt tags when in diff mode. It makes company-coq not recognize its name and hence it is not proposed as completion.
To reproduce:

(* Enable company-coq and diff-mode from here. *)
Goal forall n:nat, True.
Proof.
  intro n.
  induction n as [|x H_ind_hyp];[auto|].
  H_i (* no completion proposed *)

The last goal in *coq* is like this. I suppose that this misleads the hyp name recognition mechanism.

  <diff.added.bg><diff.added>x : nat</diff.added></diff.added.bg>
  <diff.added.bg><diff.added>H_ind_hyp : True</diff.added></diff.added.bg>
  ============================
  True

[Matafou]

From the number of issues raised by the diff mode for company-coq I suspect it relies too much on the *coq* content and should maybe migrate to looking more into *goal* and *response* instead?
Until we switch to some good protocol of course (I should have this disclaimer in my signature...).

[cpitclaudel]

Ah, good catch. I think your analysis is almost right… except I actually tried to avoid relying on buffer contents as much as possible and instead used variables like proof-shell-last-goals-output. I'm not too eager to depend on the contents of *goals* instead, because that sounds less robust; WDYT?

[Matafou]

Right, relying on this variable seems better. Maybe we could try to clean that variable from the tags in PG instead. Would it make other features fail? Otherwise we just provide a function removing these tags.

[cpitclaudel]

Would it make other features fail?

I'm not sure :) It would make it harder to implement features that need the tags. Maybe adding a filtering function is the right way to go.

[Matafou]

Yes probably. Hopefully we don't get into efficiency problems.

[erikmd]

BTW, I guess this is related to this other issue: #239