fstar-mode.el icon indicating copy to clipboard operation
fstar-mode.el copied to clipboard

Advancing does not recognize [@"substitute"] qualifier

Open tchajed opened this issue 7 years ago • 1 comments

F* has a special qualifier for KreMLin [@"substitute"] that fstar-mode doesn't recognize, so that advancing processes any definitions with this qualifier:

module Interactive_advance_substitute

(* fstar-subp-advance-next here... *)
let a = 1

[@"substitute"] let b = 2
(* ... goes here *)

This is low priority, and I'm not sure if this type of qualifier will stick around in F*.

tchajed avatar Jul 25 '17 13:07 tchajed

The fix would be to refine the predicate that's used for picking headers to start on. Currently it checks for preceding blanks and being outside of a comment.

cpitclaudel avatar Aug 03 '17 18:08 cpitclaudel