Feature request: highlight cheating commands

[tchajed]

Porting this feature from Proof General would be useful to keep track of when a proof doesn't actually work.

I think the identifiers to highlight are assume, admit(), magic, unsafe_coerce, and admitP, based on looking at prims.fst.

[cpitclaudel]

Sounds good. In the meantime, you can put this in your fstar-mode-hook:

(font-lock-add-keywords nil `((,(regexp-opt '("assume" "admit" "admitP" "magic" "unsafe_coerce") 'symbols) . font-lock-warning-face)))