       (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)

       (substitute-command-keys (format " (%s for help)" help-kbd))
     "")))

(defun fstar-subp--parse-info (response)
  "Parse info structure from RESPONSE."
  (when (string-match fstar-subp--info-response-header-regex response)

  "Show type from INFO in inline pop-up."
  (if info
      (let ((segments (delq nil (list (fstar-symbol-info-sig info)
                                      (fstar-symbol-info-docstring info)))))
        (quick-peek-show (mapconcat #'identity segments "\n\n")
                         (car (with-syntax-table fstar--fqn-at-point-syntax-table
                                (bounds-of-thing-at-point 'symbol)))))
