 (defconst fstar-known-modules
   '((font-lock        . "Syntax highlighting")
     (prettify         . "Unicode math (e.g. display forall as ∀; requires emacs 24.4 or later)")
-    (indentation      . "Indentation (based on control points)")
+    (indentation      . "Indentation (relative to previous lines)")
     (comments         . "Comment syntax and special comments ('(***', '(*+', etc.)")
     (flycheck         . "Real-time verification with Flycheck")
     (interactive      . "Interactive verification (à la Proof-General)")

    (setq prompt (format prompt default-info)))
  (read-string prompt nil nil default))

(defun fstar-in-comment-p ()
  "Return non-nil if point is inside a comment."
  (nth 4 (syntax-ppss)))

(defun fstar-subp--column-number-at-pos (pos)
  "Return column number at POS."


;;; Indentation

(defun fstar--indentation-previous-line ()
  "Go to previous non-blank line."
  (goto-char (point-at-bol))
  (skip-chars-backward " \t\n"))

(defun fstar--indentation-points-before (&optional max-column)
  "Add indentation points before MAX-COLUMN or current point to POINTS."
  (let ((points nil)
        (bol (point-at-bol)))
    (when max-column
      (move-to-column max-column))
    (while (> (point) bol)
      (skip-chars-backward " \t" bol)
      (when (/= (skip-chars-backward "^ \t" bol) 0)
        (push (current-column) points)))
    points))

(defun fstar--indentation-points ()
  "Collect indentation points for current line."
  (let ((points nil)
        (in-comment (fstar-in-comment-p (point-at-bol))))
    (save-excursion
      (while (and (not (bobp)) (> (or (car points) 1) 0))
        (fstar--indentation-previous-line)
        (let ((line-points (fstar--indentation-points-before (car points))))
          (when in-comment
            (setq line-points (-filter #'fstar--column-in-commment-p line-points)))
          (when (and (null points) line-points)
            (cl-pushnew (+ (car line-points) 2) (cdr line-points)))
          (setq points (nconc line-points points)))))
    points))

(defun fstar--indentation-insert-points ()
  "Show indentation points on current line."
  (beginning-of-line)
  (dolist (point (fstar--indentation-points))
    (move-to-column point t)
    (insert "^")))

(defun fstar--indent-1 (backwards)
  "Cycle (forwards or BACKWARDS) between relevant indentation points."
  (let* ((current-ind (current-indentation))
         (points (fstar--indentation-points))
         (pred (apply-partially (if backwards #'> #'<) current-ind))
         (remaining (or (-filter pred points) points))
         (target (car (if backwards (last remaining) remaining))))
    (if (> (current-column) current-ind)
        (save-excursion (indent-line-to target))
      (indent-line-to target))))
