 ;;; Prettify symbols
 
 (defconst fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
-                                ("nat" . ?ℕ) ("int" . ?ℤ)
-                                ("True" . ?⊤) ("False" . ?⊥)
-                                ("*" . ?×) ("~>" . ?↝)
-                                ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
-                                ("/\\" . ?∧) ("\\/" . ?∨) ("=!=" . ?≠)
-                                ("&&" . ?∧) ("||" . ?∨) ("<>" . ?≠)
-                                ("<==>" . ?⟺) ("==>" . ?⟹)
-                                ("=>" . ?⇒) ("->" . ?→)
-                                ;; ("(|" . 10629) ("|)" . 10630)
-                                ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
-                                ("'d" . ?δ) ("'e" . ?η))
+                            ("nat" . ?ℕ) ("int" . ?ℤ)
+                            ("True" . ?⊤) ("False" . ?⊥)
+                            ("*" . ?×) ("~>" . ?↝)
+                            ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
+                            ("/\\" . ?∧) ("\\/" . ?∨) ("=!=" . ?≠)
+                            ("&&" . ?∧) ("||" . ?∨) ("<>" . ?≠)
+                            ("<==>" . ?⟺) ("==>" . ?⟹)
+                            ("=>" . ?⇒) ("->" . ?→)
+                            ;; ("(|" . 10629) ("|)" . 10630)
+                            ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
+                            ("'d" . ?δ) ("'e" . ?η))
   "Fstar symbols.")
-
 
 (defun fstar-setup-prettify ()
   "Setup prettify-symbols for use with F*."

(defun fstar-subp-highlight-issue (issue)
  "Highlight ISSUE in current buffer."
  (let* ((from (fstar-issue-offset (fstar-issue-line-from issue)
                                   (fstar-issue-col-from issue)))
         (to (fstar-issue-offset (fstar-issue-line-to issue)
                                 (fstar-issue-col-to issue)))
         (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
    (overlay-put overlay 'fstar-subp-issue t)
    (overlay-put overlay 'face 'fstar-subp-overlay-issue-face)

(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (goto-char (fstar-issue-offset (fstar-issue-line-from issue)
                             (fstar-issue-col-from issue))))

(defun fstar-subp-handle-failure (response overlay)
  "Process failure RESPONSE from F* subprocess for OVERLAY."
