   (interactive)
   (mapc #'fstar--hide-buffer fstar--all-temp-buffer-names))
 
+;;; Outline
+
+(defun fstar--outline-close-and-goto (&optional _)
+  "Close occur buffer and go to position at point."
+  (interactive)
+  (let ((pos (occur-mode-find-occurrence))
+        (occur-buf (current-buffer)))
+    (switch-to-buffer (marker-buffer pos))
+    (goto-char pos)
+    (kill-buffer occur-buf)))
+
+(defun fstar--outline-cleanup (title)
+  "Clean up outline buffer and give it a proper TITLE."
+  (let ((inhibit-read-only t))
+    (goto-char (point-min))
+    (delete-region (point) (1+ (point-at-eol)))
+    (insert (fstar--propertize-title title) "\n")
+    (when (fboundp 'font-lock--remove-face-from-text-property)
+      (font-lock--remove-face-from-text-property (point) (point-max) 'face 'match))))
+
+(defvar fstar--outline-map
+  (let ((map (make-sparse-keymap)))
+    (set-keymap-parent map occur-mode-map)
+    (dolist (command '(occur-mode-goto-occurrence occur-mode-mouse-goto))
+      (substitute-key-definition command #'fstar--outline-close-and-goto map))
+    map))
+
+(defun fstar-outline ()
+  "Show an outline of the current buffer."
+  (interactive)
+  (let ((same-window-buffer-names '("*Occur*"))
+        (outline-buffer-title (format "Outline of ‘%s’\n" (buffer-name)))
+        (outline-buffer-name (format "*fstar-outline: %s*" (buffer-name))))
+    (-when-let* ((buf (get-buffer outline-buffer-name)))
+      (when (buffer-live-p buf)
+        (kill-buffer buf)))
+    (occur fstar-syntax-block-header-re)
+    (when (buffer-live-p (get-buffer "*Occur*"))
+      (with-current-buffer "*Occur*"
+        (rename-buffer outline-buffer-name t)
+        (toggle-truncate-lines t)
+        (use-local-map fstar--outline-map)
+        (fstar--outline-cleanup outline-buffer-title)))))
+
 ;;; Interactive proofs (fstar-subp)
 
 (cl-defstruct fstar-subp-query

      (fstar-subp-highlight-issues local-issues overlay)
      (display-local-help))))


;;; ;; Tracking and updating overlays


        (if (equal target-fname "<input>")
            (setq target-fname buffer-file-name))
        (fstar--navigate-to target-fname
                            (fstar-location-line-from def-loc)
                            (fstar-location-col-from def-loc)
                            display-action))
    (message "No definition found")))

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