; Copyright (C) 2003  Georgia Institute of Technology

; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

; Written by: Panagiotis Manolios who can be reached as follows.

; Email: manolios@cc.gatech.edu

; Postal Mail:
; College of Computing
; CERCS Lab
; Georgia Institute of Technology
; 801 Atlantic Drive
; Atlanta, Georgia 30332-0280 U.S.A.

; =============================================================
; Some useful settings.  Look at the manual for details
; =============================================================

(setq line-number-mode t)
(setq column-number-mode t)
(setq visible-bell t)
(setq explicit-shell-file-name "bash")

(put 'upcase-region 'disabled nil)
(put 'downcase-region 'disabled nil)

;;;  Set correct editor indentation for the functions listed.
;;;  Current indentation is returned by (get '<func> 'lisp-indent-hook).

(mapcar '(lambda (x)
	   (put x 'lisp-indent-hook 'defun))
	'(all block case do do* do-filled-array
	   dolist dolist-numbered domap domap-numbered dotimes
	   ecase etypecase eval-when exists exporting-defstruct
	   labels let let* multiple-value-bind mvbind mvsetq
	   nd-rule prog1 return-from rule-bind term-bind typecase
	   unless unwind-protect when with-open-file))

;;; Cause editor to indent first 3 forms following an 'if.

(put 'if 'lisp-indent-hook 3)

; =============================================================
; Here are the functions that you have seen me use in class.
; Again, consult the Emacs manual for details.
;
; The functions that you want to call from the top level are the
; ones which are interactive. They are also key bindings for such
; functions (scan for "(global-set-key").
; 
; Functions which are not interactive are helper functions and
; can be ignored.
; =============================================================

(defun center0 ()
  "Redraw screen with pointer at beginning of screen"
  (interactive)
  (recenter 0))

; So Ctrl-x-l invokes the centre0 function.
(global-set-key "\C-xl" 'center0)

; This variable, which you can set with set-acl2-active-shell-buffer,
; keeps track of the name of the active ACL2 shell buffer.
(defvar acl2-active-shell-buffer "*shell*"
  "*Used by send-acl2-form to send the current acl2 form to the active shell buffer")

; This variable, which you can set with set-acl2-active-input-buffer,
; keeps track of the name of the active ACL2 input buffer.
(defvar acl2-active-input-buffer "*scratch*"
  "*Used by get-acl2-form to get the next s-expression from the active input buffer")

(defun set-acl2-active-shell-buffer ()
  "Make the current buffer the active acl2 shell buffer"
  (interactive)
  (setq acl2-active-shell-buffer
	(buffer-name)))

(global-set-key "\C-xas" 'set-acl2-active-shell-buffer)

(defun set-acl2-active-input-buffer ()
  "Make the current buffer the active acl2 input buffer"
  (interactive)
  (setq acl2-active-input-buffer
	(buffer-name)))

(global-set-key "\C-xai" 'set-acl2-active-input-buffer)

(defun skip-white-space ()
  (while (looking-at "[ \t\n]")
    (forward-char 1)))

(defun skip-nested-comments (depth)
  (cond 
   ((< depth 1) t)
   (t (re-search-forward "|#\\|#|" (point-max) t 1)
      (forward-char -2)
      (cond ((looking-at "#|")
	     (forward-char 2)
	     (skip-nested-comments (1+ depth)))
	    (t (forward-char 2)
	       (skip-nested-comments (1- depth)))))))

(defun skip-comments ()
  (cond ((looking-at ";")
	 (beginning-of-line 2)
	 (skip-comments))
	((looking-at "#|")
	 (forward-char 2)
	 (skip-nested-comments 1)
	 (skip-comments))
	((looking-at "[ \t\n]")
	 (skip-white-space)
	 (skip-comments))
	(t t)))

; This is the function that allows you to send the sexpression
; from the point to the acl2-active-shell-buffer. So, in the
; script buffer, position the point at the sexp you want to send
; to the ACL2 buffer and press "Alt-n" (or "Meta-n").
(defun send-acl2-form ()
  "Send the sexpt starting from the point to acl2-active-shell-buffer"
  (interactive)
  (skip-comments)
  (let ((begin (point))
	(end))
    (forward-sexp)
    (setq end (point))
    (process-send-region acl2-active-shell-buffer begin end)
    (process-send-string acl2-active-shell-buffer "\C-j")
    (accept-process-output))
  (skip-comments))

(global-set-key "\M-n" 'send-acl2-form)

; This is the function that allows you to pull in to a buffer
; running ACL2 the next sexpression form the
; acl2-active-input-buffer.
(defun get-acl2-form ()
  "Get the next sexpt from acl2-active-input-buffer"
  (interactive)
  (let ((current-buffer (buffer-name))
	(begin (point)))
    ; the next few lines are what allow me to skip past 
    ; some forms I don't want.  I check to see if I already have
    ; an sexp and if so, I delete it and get the next one.
    (forward-char -1)
    (if (looking-at ")")
	(progn 
	  (forward-char 1)
	  (forward-sexp -1)
	  (kill-region (point) begin))
      (forward-char 1))
    (switch-to-buffer acl2-active-input-buffer)
    (let ((begin (point))
	  (end nil)
	  (form nil))
      (skip-comments)
      (setq begin (point))
      (forward-sexp 1)
      (setq end (point))
      (copy-region-as-kill begin end)
      (forward-sexp 1)
      (forward-sexp -1)
      (switch-to-buffer current-buffer)
      (goto-char (point-max))
      (insert "\C-j")
      (yank)
      (goto-char (point-max)))))

(global-set-key "\C-\M-n" 'get-acl2-form)

; This function is used to untabify sexpressions. It is useful
; when you are cutting and pasting text, say into Latex, and
; don't want tabs, as they cause formatting problems.
(defun indent-untabify-sexp ()
  "Indent an s-expression and untabify it."
  (interactive)
  (save-excursion
    (indent-sexp)
    (let ((begin (point)))
      (forward-sexp 1)
      (untabify begin (point)))))

(global-set-key "\C-\M-q" 'indent-untabify-sexp)