Search results incorrectly highlighted as errors

[Tuplanolla]

Versions

Coq 8.15.0

Coqtail 1.6.2

Vim 8.2

Equations 1.3

Python 3.7.4

Description

Search results for lemmas, whose names end in error, are highlighted as if they were errors themselves. Check the following script and observe the result.

From Coq Require Import Lists.List.

Search nth_error.

nth_error_In:
  forall [A : Type] (l : list A) (n : nat) [x : A],
  nth_error l n = Some x -> In x l

nth_error_repeat:
  forall [A : Type] (a : A) [m n : nat],
  n < m -> nth_error (repeat a m) n = Some a

In_nth_error:
  forall [A : Type] (l : list A) (x : A),
  In x l -> exists n : nat, nth_error l n = Some x

nth_error_None:
  forall [A : Type] (l : list A) (n : nat),
  nth_error l n = None <-> length l <= n

[Tuplanolla]

Also, lemmas and variables, whose names start with exists, are highlighted as if they were quantifiers.

From Coq Require Import Lists.List.

Search existsb.

existsb_app:
  forall [A : Type] (f : A -> bool) (l1 l2 : list A),
  existsb f (l1 ++ l2) = (existsb f l1 || existsb f l2)%bool

existsb_exists:
  forall [A : Type] (f : A -> bool) (l : list A),
  existsb f l = true <-> (exists x : A, In x l /\ f x = true)

existsb_nth:
  forall [A : Type] (f : A -> bool) (l : list A) [n : nat] (d : A),
  n < length l -> existsb f l = false -> f (nth n l d) = false

[Tuplanolla]

Word boundaries are not enough to tame the standard library, because the following search still breaks the highlighting.

Search option.

error: forall {A : Type}, option A

None: forall {A : Type}, option A

value: forall [A : Type], A -> option A

Some: forall {A : Type}, A -> option A

[whonore]

Good point. In that case I think a simple regex isn't going to be able to distinguish an actual error message and an identifier/notation that resembles an error message. Coqtail knows the difference when it gets a response from Coq, but then forgets when everything gets mixed together in the Info panel.

A few relatively simple options I can think of are:

1. Keep the Info panel as-is, but add a special prefix to error messages so they can be recognized by the syntax highlighting. This is probably the easiest choice, but is still somewhat fragile since someone could potentially still use the prefix as an identifer/notation and we'd have the same problem as now.
2. Change the type of the Info panel from list string to something like list (string * msg_type) where msg_type = Msg | Error. Then, when it comes time to actually put text in a Vim buffer, group all the error messages in a special section of the buffer (e.g. at the top with a header like Errors: and ending with ------) and teach the syntax highlighting regex to recognize everything in that block as an error.
3. Change the type of the Info panel as in option 2, but instead of relying on syntax highlighting, use matchadd to highlight errors appropriately. This has a lot in common with the current proof diff highlighting in the Goal panel.