 
 ;;; ;; ;; Tactics
 
+(cl-defstruct fstar-proof-state
+  label goals smt-goals)
+
 (defconst fstar--goals-buffer-name "*fstar: goals*")
 (push fstar--goals-buffer-name fstar--all-temp-buffer-names)
 

       (with-selected-window window
         (recenter 0)))))

(defun fstar-tactics--display-proof-state (proof-state)
  "Display PROOF-STATE in a separate *goals* buffer."
  (let ((help-window-select nil))
    (fstar-tactics--with-goals-buffer
      (goto-char (point-max))
      (save-excursion
        (fstar-tactics--insert-proof-state proof-state))
      (unless (bobp) (forward-line 2)))))

;;; ;; Starting the F* subprocess

      (fstar-tactics--insert-goal goal)
      (insert "\n"))))

(defun fstar-tactics--insert-proof-state (ps)
  "Dump proof state PS into current buffer."
  (unless (bobp)
    (fstar--insert-with-face 'fstar-proof-state-separator-face
        (propertize "\n" 'line-prefix "" 'line-height t))
    (insert "\n"))
  (fstar--insert-with-face 'fstar-proof-state-header-face
      (propertize (or (fstar-proof-state-label ps) "…")
                  'line-prefix "" 'wrap-prefix "" 'fstar--header t))
  (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))
  (insert (propertize "\n" 'line-spacing 0.2))
  (fstar-tactics--insert-goals (fstar-proof-state-goals ps) "Goal")
  (fstar-tactics--insert-goals (fstar-proof-state-smt-goals ps) "SMT goal"))

(defun fstar-tactics--next-proof-state (&optional n)
  "Go forward N goals (default: 1)."
