 
 (defun fstar-subp--process-message (level contents)
   "Process CONTENTS of real-time feedback message at LEVEL."
-  (let ((header (format "[F* %s] " level)))
-    (setq contents (string-trim contents))
-    (message "%s" (fstar--indent-str contents header))))
+  (pcase level
+    ("proof-state" (fstar-subp-tactics--display-proof-state contents))
+    (_ (let ((header (format "[F* %s] " level)))
+         (unless (stringp contents)
+           (setq contents (prin1-to-string contents)))
+         (message "%s" (fstar--indent-str (string-trim contents) header))))))
 
 (defun fstar-subp--process-protocol-info (_vernum proto-features)
   "Register information (VERNUM and PROTO-FEATURES) about the protocol."

  "Remove leftover hooks from proof completion notifications."
  (remove-hook 'focus-in-hook #'fstar--notify-focus-in)
  (remove-hook 'focus-out-hook #'fstar--notify-focus-out))

;;; ;; Starting the F* subprocess


  "Run BODY widened in a `save-excursion' block."
  (declare (indent 0) (debug t))
  `(save-excursion (save-restriction (prog-widen) ,@body)))

(defun fstar--specified-space-to-align-right (str)
  "Compute a specified space to align STR to the right."
  (let ((str-width (string-width str)))
    (propertize " " 'display `(space :align-to (- right ,str-width)))))

(defun fstar--insert-with-face (face fmt &rest args)
  "Insert (format FMT args) with FACE."
  (declare (indent 2))
  (let ((beg (point)))
    (insert (apply #'format fmt args))
    (font-lock-append-text-property beg (point) 'face face)))

(defun fstar--insert-ln-with-face (face fmt &rest args)
  "Insert (format FMT args) with FACE."
  (declare (indent 2))
  (apply #'fstar--insert-with-face face fmt args)
  (insert "\n"))

;;; Debugging

