FStarLang / fstar-mode.el

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

Advancing skips over definitions with qualifiers on a separate line #63

Closed tchajed closed 7 years ago

tchajed commented 7 years ago

Here's an example:

module Interactive_advance_quals

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

unfold
let b = 2

unfold
let c = 3

(* ... goes here *)
unfold let d = 4

Note that it recognizes the unfold let d and stops, but misses the definitions that put the qualifiers on a separate line. I might tend to put unfold on the same line as the let or val, but inline_for_extract I usually want on a separate line.

cpitclaudel commented 7 years ago

Indeed, thanks