; Adapted from the script for the flying demo....

; The following should be carried out before the demo starts.  It consists of
; commands to configure emacs.

; (1) Fire up an emacs on this directory.  Put the .lisp file in one buffer.
; Set up a shell buffer named *shell*.  Run acl2 in that shell.

; (2) Execute the following Emacs Lisp code.  You can do this by
; grabbing the s-expression below and typing meta-: ctrl-y Return,
; i.e., yank the s-expression into the Emacs Eval command.

(progn
  (fset 'scroll-acl2-prompt-to-top
   "\C-r!>\M-0\C-l\C-x\C-x")
  (fset 'back-to-acl2-prompt
   "\C-r!>\C-r\C-f\C-f\M-0\C-l\C-a")
  (fset 'back-to-end-of-buffer
        "\M->")
  (defun yank-sexp-into-shell ()
    "Yanks current sexp into the buffer named *shell*"
    (interactive)
    (forward-char)
    (beginning-of-defun)
    (let ((pos (point))) 
      (forward-sexp)
      (end-of-line) ; pick up comment
      (kill-ring-save pos (point)))
    (forward-char) ; probably sometimes necessary to step past #| .. |#
    (end-of-defun) ; rather than (forward-sexp), since we stepped forward a character
    (backward-sexp)
    (switch-to-buffer "*shell*")
    (goto-char (point-max))
    (yank)
    ;; Pretty up the input:
    (backward-sexp)
    (indent-sexp)
    (goto-char (point-max)))
  
  (fset 'yank-sexpr-into-shell-from-last-buffer-visited
        "\C-xb\C-m\M-xyank-sexp-into-shell")

  (global-set-key "[" 'scroll-acl2-prompt-to-top)
  (global-set-key "{" 'back-to-acl2-prompt)
  (global-set-key "\M-[" 'back-to-acl2-prompt)
  (global-set-key "\M-]" 'back-to-end-of-buffer)
  (global-set-key "]" 'yank-sexpr-into-shell-from-last-buffer-visited))

; This s-expression above sets up the following emacs commands.
;  [   to move the current acl2 prompt line to the top and
;  ]   to yank the next event from this file into the shell.
;  M-[ to return to last prompt

; (4) Position the Emacs cursor just before the first form in the .lisp file to
; be executed.  Change to buffer *shell* (which has ACL2 running in it), hit
; \M-] to go to the bottom of the buffer, and then get started.