 (defun fstar--navigate-to-1 (location display-action switch)
   "Navigate to LOCATION.
 DISPLAY-ACTION determines where the resulting buffer is
-shown (nil for the currently selected window, `window' for a
-separate window, and `frame' for a separate frame).  SWITCH
-determines whether the resulting buffer and window become current
-and selected."
+shown (nil for the currently selected window, `reuse' for the
+current window unless another one is already showing the buffer,
+`window' for a separate window, and `frame' for a separate
+frame).  SWITCH determines whether the resulting buffer and
+window become current and selected."
   (fstar--push-mark)
   (let ((fname (fstar-location-filename location))
         (line (fstar-location-line-from location))

(defun fstar--navigate-to-parse-display-action (display-action)
  "Convert DISPLAY-ACTION into an argument to `display-buffer'."
  (pcase display-action
    (`nil '((display-buffer-same-window display-buffer-reuse-window)))
    (`window '((display-buffer-reuse-window display-buffer-pop-up-window)
               (reusable-frames . 0)
               (inhibit-same-window . t)))

    (save-excursion
      (insert title "\n")
      (when def-loc
        (fstar--insert-link def-loc '(:height 0.9 :inherit link) nil 'reuse))
      (cl-etypecase info
        (fstar-symbol-info
         (-when-let* ((type (fstar-symbol-info-type info)))
