 (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)))
+    (`nil '((display-buffer-same-window)))
+    (`reuse '((display-buffer-reuse-window display-buffer-same-window)))
     (`window '((display-buffer-reuse-window display-buffer-pop-up-window)
                (reusable-frames . 0)
                (inhibit-same-window . t)))

    (insert (fstar--propertize-title title) "\n\n"))
  (dolist (fname deps)
    (insert "  ")
    (fstar--insert-link fname 'default)
    (insert "\n")))

(defun fstar-subp--visit-dependency-continuation (source-buf status response)

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