 
 ;;; ;; ;; Jump to definition
 
-(defun fstar--save-point ()
-  "Save current position in mark ring and xref stack."
-  (push-mark nil t)
-  (when (fboundp 'xref-push-marker-stack)
-    (xref-push-marker-stack)))
-
 (defun fstar--jump-to-definition-continuation (display-action info)
   "Jump to position in INFO.
 DISPLAY-ACTION indicates how: nil means in the current window;

                   (`(,target-row . ,target-col) (fstar-lookup-result-def-start info)))
        (when (equal target-fname "<input>")
          (setq target-fname buffer-file-name))
        (fstar--save-point)
        (catch 'not-found
          (unless (file-exists-p target-fname)
            (message "File not found: %S" target-fname)
            (throw 'not-found nil))
          (pcase display-action
            (`nil (find-file target-fname))
            (`window (find-file-other-window target-fname))
            (`frame (find-file-other-frame target-fname)))
          (fstar--goto target-row target-col)
          (recenter)
          (when (fboundp 'pulse-momentary-highlight-one-line)
            (pulse-momentary-highlight-one-line (point)))))
    (message "No definition found")))

(defun fstar-jump-to-definition-1 (pos disp)

(defun fstar--propertize-title (title)
  "Format TITLE as a title."
  (propertize title 'face '(:height 1.5)))

(defun fstar--push-mark ()
  "Save current position in mark ring and xref stack."
  (push-mark nil t)
  (when (fboundp 'xref-push-marker-stack)
    (xref-push-marker-stack)))

(defun fstar--navigate-to (fname line col 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
`frame' for a new frame)."
  (fstar--push-mark)
  (catch 'not-found
    (unless (file-exists-p fname)
      (message "File not found: %S" fname)
      (throw 'not-found nil))
    (pcase display-action
      (`nil (find-file fname))
      (`window (find-file-other-window fname))
      (`frame (find-file-other-frame fname)))
    (fstar--goto-line-col line col)
    (recenter)
    (when (fboundp 'pulse-momentary-highlight-one-line)
      (pulse-momentary-highlight-one-line (point)))))

;;; Debugging

