search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

Highlighting from SMT solver responses obscures precise error feedback #71

Closed tchajed closed 6 years ago

tchajed commented 7 years ago

F* now gives general feedback about why the SMT solver failed, which does not have a precise location, sometimes in addition to giving a precise assertion failure. It's hard to see the error highlight (red) with the warning highlighting (orange):

screen shot 2017-08-15 at 10 26 57 am

Line 67 has an error overlay for off where there's a good subtyping checked failed error, but it's barely visible.

Perhaps the warning overlay should not be applied if there's an error in the same range? That or the error+warning face should be more distinct than the adjacent warning face.

cpitclaudel commented 7 years ago

Yuck yuck. Thanks for pointing the problem out. Can you provide an example input file, so I can experiment with solutions?

cpitclaudel commented 7 years ago

Ping :)