   (fstar--insert-with-face 'fstar-proof-state-header-face
       (propertize (or (fstar-proof-state-label ps) "…")
                   'line-prefix "" 'wrap-prefix "" 'fstar--header t))
+  (when (fstar-proof-state-location ps)
+    (insert " @ ")
+    (fstar--insert-link (fstar-proof-state-location ps) 'link 'window))
   (let ((timestamp (current-time-string)))
     (insert " " (fstar--specified-space-to-align-right timestamp 1))
     (fstar--insert-with-face 'fstar-proof-state-header-timestamp-face timestamp))

  (let-alist json
    (make-fstar-proof-state
     :label (if (equal .label "") nil .label)
     :goals .goals
     :smt-goals .smt-goals)))


;;; ;; ;; Tactics

(cl-defstruct fstar-proof-state
  label location goals smt-goals)

(defconst fstar--goals-buffer-name "*fstar: goals*")
(push fstar--goals-buffer-name fstar--all-temp-buffer-names)
