             (backward-sexp 1))))
     (error (forward-char -1))))
 
-(defun sl-comment-indent ()
+(defun sw:comment-indent ()
   (if (looking-at "^(\\*")              ; Existing comment at beginning
       0                                 ; of line stays there.
     (save-excursion


  ;; Process commands added to specware-mode-map -- these should autoload
;;;  (define-key map "\C-c\C-s" 'switch-to-sl)
;;;  (define-key map "\C-c\C-l" 'sl-load-file)
;;;  (define-key map "\C-c\C-r" 'sl-send-region)
;;;  (define-key map "\C-c\C-b" 'sl-send-buffer)
;;;  (define-key map "\C-c`"    'sl-next-error)
  )

(defvar sl-no-doc
  "This function is part of sl-proc, and has not yet been loaded.
Full documentation will be available after autoloading the function."
  "Documentation for autoload functions.")

;;;(autoload 'switch-to-sl   "sl-proc"   sl-no-doc t)
;;;(autoload 'sl             "sl-proc"   sl-no-doc t)
;;;(autoload 'sl-load-file   "sl-proc"   sl-no-doc t)
;;;(autoload 'sl-send-region "sl-proc"   sl-no-doc t)
;;;(autoload 'sl-send-buffer "sl-proc"   sl-no-doc t)
;;;(autoload 'sl-next-error  "sl-proc"   sl-no-doc t)

(defvar specware-mode-map nil "The mode map used in specware-mode.")
(cond ((not specware-mode-map)
       (setq specware-mode-map (make-sparse-keymap))
       (install-sl-keybindings specware-mode-map)))

;;;(and fi:lisp-listener-mode-map
;;;     (install-sl-keybindings fi:lisp-listener-mode-map))

      (max (1+ (current-column))        ; Else indent at comment column
           comment-column))))           ; except leave at least one space.

;;; INSERTING PROFORMAS (COMMON SW FORMS) 

(defconst sw:form-alist
  '(("let") ("datatype")
    ("case"))
  "The list of regions to auto-insert.")

(defun sw:insert-form ()
  "Interactive short-cut to insert a common Specware form."
  (interactive)
  (let ((newline nil)                   ; Did we insert a newline
        (name (completing-read "Form to insert: (default let) "
                               sw:form-alist nil t nil)))
    ;; default is "let"
    (if (string= name "") (setq name "let"))
    ;; Insert a newline if point is not at empty line
    (sw:indent-line)                   ; Indent the current line
    (if (save-excursion (beginning-of-line) (skip-chars-forward "\t ") (eolp))
        ()
      (setq newline t)
      (insert "\n"))
    (condition-case ()
        (cond
         ((string= name "let") (sw:let))
         ((string= name "functor") (sw:functor))
         ((string= name "case") (sw:case))
         ((string= name "datatype") (sw:datatype)))
      (quit (if newline 
                (progn
                  (delete-char -1)
                  (beep)))))))

(defun sw:let () 
  "Insert a `let in end'."
  (sw:let-local "let"))

(defun sw:case ()
  "Insert a case, prompting for case-expresion."
  (let (indent (expr (read-string "Case expr: ")))
    (insert (concat "case " expr))
    (sw:indent-line)
    (setq indent (current-indentation))
    (end-of-line)
    (if sw:case-indent
        (progn
          (insert "\n")
          (indent-to (+ 2 indent))
          (insert "of "))
      (insert " of\n")
      (indent-to (+ indent sw:indent-level)))
    (save-excursion (insert " -> "))))


(defun sw:let-local (starter)
  (let (indent)
    (insert starter)
    (sw:indent-line)
    (setq indent (current-indentation))
    (end-of-line)
    (insert "\n") (indent-to (+ sw:indent-level indent))
    (insert "\n") (indent-to indent)
    (insert "in\n") (indent-to (+ sw:indent-level indent)) (previous-line 1) (end-of-line)))

(defun sw:functor ()
  "Insert `functor ? () : ? = struct end', prompting for name/type."
  (let (indent
        (name (read-string "Name of functor: "))
        (signame (read-string "Signature type of functor: ")))
    (insert (concat "functor " name " () : " signame " ="))
    (sw:indent-line)
    (setq indent (current-indentation))
    (end-of-line)
    (insert "\n") (indent-to (+ sw:indent-level indent))
    (insert "struct\n")
    (indent-to (+ (* 2 sw:indent-level) indent))
    (insert "\n") (indent-to (+ sw:indent-level indent))
    (insert "end") (previous-line 1) (end-of-line)))

(defun sw:datatype ()
  "Insert a `datatype ??? =', prompting for name."
  (let (indent 
        (type (read-string (concat "Type of datatype (default none): ")))
