 (defun fstar--indentation-previous-line ()
   "Go to previous non-blank line."
   (goto-char (point-at-bol))
-  (skip-chars-backward " \t\n"))
+  (skip-chars-backward fstar--spaces))
 
 (defun fstar--indentation-points-before (&optional max-column)
   "Add indentation points before MAX-COLUMN or current point to POINTS."

into blocks; process it as one large block instead."
  (interactive "P")
  (fstar-subp-start)
  (let ((limit (fstar-subp-unprocessed-beginning)))
    (cond
     ((<= (point) limit) (fstar-subp-retract-until (point)))
     ((>  (point) limit) (if (consp arg)
                             (fstar-subp-enqueue-until (point))
                           (fstar-subp-advance-until (point)))))))

(defun fstar-subp-advance-or-retract-to-point-lax (&optional arg)
  "Like `fstar-subp-advance-or-retract-to-point' with ARG, in lax mode."

(defun fstar--lispify-null (x)
  "Return X, or nil if X is `:json-null'."
  (unless (eq x :json-null) x))

(defun fstar--comment-beginning (pos)
  "Exit comment at POS, putting point before its start."
  (goto-char (nth 8 (syntax-ppss pos))))

(defun fstar--comment-end (pos)
  "Exit comment at POS, putting point after its end.
Return nil if the comment is incomplete.  Needs a call to
`fstar-setup-comments'."
  (fstar--comment-beginning pos)
  (forward-comment 1))

(defun fstar--search-predicated-1 (search-fn test-fn move-fn re)
  "Search for RE.
SEARCH-FN should go to the next match.  TEST-FN is used to
further filter matches; it is called with (match-beginning 0).
MOVE-FN is used to move the point when TEST-FN returns nil.
Return point at end of match if RE can be found, and nil
otherwise.  Position of point after calling this function is
unspecified."
  (catch 'found
    (while (funcall search-fn re nil t)
      (let ((anchor (match-beginning 0)))
        (when (funcall test-fn anchor)
          ;; Looks like we found a match 💃
          (throw 'found (point)))
        (unless (funcall move-fn)
          ;; No way to make progress 😱 It's crucial to exit early here —
          ;; otherwise, we could infloop by repeatedly matching eob.
          (throw 'found nil))))
    ;; No results 😐
    (throw 'found nil)))

(defun fstar--search-predicated (search-fn test-fn move-fn re)
  "Search for RE.
SEARCH-FN should go to the next match.  TEST-FN is used to
further filter matches; it is called with (match-beginning 1).
MOVE-FN is used to move the point when TEST-FN returns nil.
Return point at end of match if RE can be found, and nil
otherwise.  This function does not move the point."
  (save-excursion
    (and (fstar--search-predicated-1 search-fn test-fn move-fn re)
         ;; Ensure that match is maximal (if the buffer contains \n•\n then
         ;; (re-search-backward "\n+") produces a match that ends at point (•),
         ;; and doesn't include the following \n)
         (goto-char (match-beginning 0))
         (looking-at re))))

(defun fstar--adjust-point-forward ()
  "Move point forward and return a boolean indicating success."
  (unless (eobp) (forward-char) t))

(defun fstar--search-predicated-forward (test-fn re)
  "Search forward for RE.
TEST-FN is used to further filter matches; it is called
with (match-beginning 1)."
  (fstar--search-predicated #'re-search-forward test-fn
                       #'fstar--adjust-point-forward re))

(defun fstar--adjust-point-backward ()
  "Move point backward and return a boolean indicating success."
  (unless (bobp) (backward-char) t))

(defun fstar--search-predicated-backward (test-fn re)
  "Search backward for RE.
TEST-FN is used to further filter matches; it is called
with (match-beginning 1)."
  (fstar--search-predicated #'re-search-backward test-fn
                       #'fstar--adjust-point-backward re))

;;; Debugging

