       (with-no-warnings (font-lock-fontify-buffer)))
     (buffer-string)))
 
+(defun fstar--highlight-docstring-buffer ()
+  "Highlight current buffer as an F* docstring."
+  (let ((inhibit-read-only t))
+    (goto-char (point-min))
+    (while (search-forward "[" nil t)
+      (let* ((beg (point))
+             (end (ignore-errors (backward-char) (forward-sexp) (1- (point))))
+             (str (and end (buffer-substring-no-properties beg end))))
+        (if (null str)
+            (goto-char (point-max))
+          (goto-char beg)
+          (delete-region beg end)
+          (insert (fstar-highlight-string str)))))))
+
+(defun fstar--highlight-docstring (str)
+  "Highlight STR as an F* docstring."
+  (with-temp-buffer
+    (insert str)
+    (fstar--highlight-docstring-buffer)
+    (buffer-string)))
+
 (defun fstar-setup-font-lock ()
   "Setup font-lock for use with F*."
   (font-lock-mode -1)

  "Show documentation in INFO."
  (-if-let* ((doc (and info (fstar-symbol-info-doc info))))
      (with-help-window fstar--doc-buffer-name
        (princ doc))
    (message
     (substitute-command-keys "No documentation found. \
Try visiting the source file with \\[fstar-jump-to-definition]?"))))

eldoc to show the type of the whole *before* destruction, not
after."
  (eldoc-print-current-symbol-info))

(defun fstar--unwrap-paragraphs (str)
  "Remove hard line wraps from STR."
  (replace-regexp-in-string "\n\\([^\n\t ]\\)" "\\1" str))

;;; Debugging

