 
 ;;; Utilities
 
-(defun fstar--indent-str (str amount)
-  "Indent all newlines of STR by AMOUNT."
-  (replace-regexp-in-string "\n" (concat "\n" (make-string amount ?\s)) str))
+(defun fstar--indent-str (str amount &optional skip-first-line)
+  "Indent all lines of STR by AMOUNT.
+If AMOUNT is a string, use that as indentation.
+With SKIP-FIRST-LINE, don't indent the first one."
+  (let ((indent (if (stringp amount) amount (make-string amount ?\s))))
+    (if skip-first-line
+        (replace-regexp-in-string "\n" (concat "\n" indent) str)
+      (replace-regexp-in-string "^" indent str))))
 
 (defun fstar--property-range (pos prop)
   "Find range around POS with consistent non-nil value of PROP."

      (let* ((name-str (car branches))
             (branch-strs (mapconcat #'fstar--format-one-branch (cdr branches) "\n"))
             (match (format "match ${%s} with\n%s" name-str branch-strs))
             (indented (fstar--indent-str match (current-column))))
        (let ((yas-indent-line nil))
          (fstar--expand-snippet (fstar--prepare-match-snippet indented))))
    (message "No match found for type `%s'." type)))

            (propertize  "\n" 'line-height `(nil . 1.5) 'line-spacing 0.2))
    (let ((from (point))
          (type (fstar--unparens .type)))
      (insert (fstar-highlight-string (fstar--indent-str type 2)))
      (font-lock-append-text-property from (point) 'face '(:height 0.9)))))

(defun fstar-subp--search-continuation (terms status response)
