 ;; * Syntax highlighting
 ;; * Unicode math (prettify-symbols-mode)
 ;; * Documentation and search
-;; * Simple indentation
+;; * Relative indentation
 ;; * Type hints (Eldoc)
 ;; * Autocompletion (Company)
 ;; * Type-aware snippets (Yasnippet)


;;; Indentation

(defun fstar-comment-offset ()
  "Compute offset at beginning of comment."
  (comment-normalize-vars)
  (when (fstar-in-comment-p)
    (save-excursion
      (comment-beginning)
      (- (point) (point-at-bol)))))

(defun fstar-indentation-points ()
  "Find reasonable indentation points on the current line."
  (let ((points))
    (save-excursion
      (when (= (forward-line -1) 0) ;; Recognize the first line
        (while (re-search-forward "\\s-+" (point-at-eol) t)
          (push (current-column) points))))
    (when points
      (let ((mn (apply #'min points)))
        (push (+ 2 mn) points)
        (push (+ 4 mn) points)))
    (push 0 points)
    (push 2 points)
    (-when-let* ((comment-offset (fstar-comment-offset)))
      (setq points (-filter (lambda (pt) (>= pt comment-offset))
                            (cons comment-offset points))))
    (-distinct (sort points #'<))))

(defun fstar--indent-1 (backwards)
  "Cycle between vaguely relevant indentation points.
With BACKWARDS, go back among indentation points."
  (let* ((current-ind (current-indentation))
         (points (fstar-indentation-points))
         (remaining (or (-filter (if backwards
                                     (lambda (x) (< x current-ind))
                                   (lambda (x) (> x current-ind)))
                                 points)
                        points))
         (target (car (if backwards
                          (last remaining)
                        remaining))))
    (if (> (current-column) current-ind)
        (save-excursion (indent-line-to target))
      (indent-line-to target))))

(defconst fstar-known-modules
  '((font-lock        . "Syntax highlighting")
    (prettify         . "Unicode math (e.g. display forall as ∀; requires emacs 24.4 or later)")
    (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)")
