 
 (defun fstar--visit-link-target (marker)
   "Jump to file indicated by entry at MARKER."
-  (find-file (get-text-property (marker-position marker)
-                                'fstar--target (marker-buffer marker))))
+  (let* ((pos (marker-position marker))
+         (buf (marker-buffer marker))
+         (target (get-text-property pos 'fstar--target buf)))
+    (cond
+     ((stringp target)
+      (find-file target))
+     ((fstar-location-p target)
+      (fstar--navigate-to (fstar-location-filename target)
+                     (fstar-location-line-from target)
+                     (fstar-location-col-from target))))))
+
+(defun fstar--insert-link (label target face)
+  "Insert a link to TARGET with LABEL and FACE.
+TARGET is either a string or a location."
+  (insert-text-button label 'fstar--target target
+                      'face face 'follow-link t
+                      'action 'fstar--visit-link-target))
 
 (defun fstar--lispify-null (x)
   "Return X, or nil if X is `:json-null'."

    (insert (fstar--propertize-title title) "\n\n"))
  (dolist (fname deps)
    (insert "  ")
    (insert-text-button fname 'fstar--target fname
                        'face 'default 'follow-link t
                        'action 'fstar--visit-link-target)
    (insert "\n")))

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

  (when (fboundp 'xref-push-marker-stack)
    (xref-push-marker-stack)))

(defun fstar--navigate-to (fname line col &optional display-action)
  "Navigate to LINE, COL of FNAME.
DISPLAY-ACTION determines where the resulting buffer is
shown (nil for same window, `window' for a new window, and
