path: root/twelf/twelf-old.el

;; twelf-old.el  Port of old Twelf Emacs mode
;;
;; Author: Frank Pfenning
;;	   Adapted for Proof General by David Aspinall <David.Aspinall@ed.ac.uk>
;;
;; $Id$
;;
;;

;; FIXME: have copied over directly!

;;; Modes and utilities for Twelf programming.  This package supports (1)
;;; editing Twelf source files with reasonable indentation, (2) managing
;;; configurations of Twelf source files, including TAGS tables, (3)
;;; communication with an inferior Twelf server to type-check and execute
;;; declarations and queries, (4) interaction with an inferior Twelf process
;;; in SML.
;;;
;;; For documentation, type C-h m in Twelf mode, or see the function
;;; twelf-mode below
;;;
;;; Author: Frank Pfenning
;;; Thu Oct 7 19:48:50 1993 (1.0 created)
;;; Fri Jan 6 09:06:38 1995 (2.0 major revision)
;;; Tue Jun 16 15:49:31 1998 (3.0 major revision)
;;;
;;;======================================================================
;;; For the `.emacs' file (copied from init.el)
;;;======================================================================
;;;
;;; ;; Tell Emacs where the Twelf libraries are.
;;; (setq load-path
;;;       (cons "/afs/cs/project/twelf/research/twelf/emacs" load-path))
;;;
;;; ;; Autoload libraries when Twelf-related major modes are started.
;;; (autoload 'twelf-mode "twelf" "Major mode for editing Twelf source." t)
;;; (autoload 'twelf-server "twelf" "Run an inferior Twelf server." t)
;;; (autoload 'twelf-sml "twelf" "Run an inferior Twelf-SML process." t)
;;;
;;; ;; Switch buffers to Twelf mode based on filename extension,
;;; ;; which is one of .elf, .quy, .thm, or .cfg.
;;; (setq auto-mode-alist
;;;       (cons '("\\.elf$" . twelf-mode)
;;;	    (cons '("\\.quy$" . twelf-mode)
;;;		  (cons '("\\.thm$" . twelf-mode)
;;;			(cons '("\\.cfg$" . twelf-mode)
;;;			      auto-mode-alist)))))
;;;
;;; ;; Default Twelf server program location
;;; (setq twelf-server-program
;;;       "/afs/cs/project/twelf/research/twelf/bin/twelf-server")
;;;
;;; ;; Default Twelf SML program location
;;; (setq twelf-sml-program
;;;       "/afs/cs/project/twelf/misc/smlnj/bin/sml-cm")
;;;
;;; ;; Default documentation location (in info format)
;;; (setq twelf-info-file
;;;       "/afs/cs/project/twelf/research/twelf/doc/info/twelf.info")
;;;
;;; ;; Automatically highlight Twelf sources using font-lock
;;; (add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer)
;;;
;;;======================================================================
;;; Command Summary
;;;======================================================================
;;;
;;; Quick summary of Twelf mode, generated from C-h b:
;;;
;;; --- Editing Commands ---
;;; TAB          twelf-indent-line
;;; DEL          backward-delete-char-untabify
;;; M-C-q        twelf-indent-decl
;;;
;;; --- Type Checking ---
;;; C-c C-c      twelf-save-check-config
;;; C-c C-s      twelf-save-check-file
;;; C-c C-d      twelf-check-declaration
;;; C-c c        twelf-type-const
;;; C-c C-u      twelf-server-display
;;;
;;; --- Error Tracking ---
;;; C-c `        twelf-next-error
;;; C-c =        twelf-goto-error
;;;
;;; --- Syntax Highlighting ---
;;; C-c C-l      twelf-font-fontify-decl
;;; C-c l        twelf-font-fontify-buffer
;;;
;;; --- Server State ---
;;; C-c <        twelf-set
;;; C-c >        twelf-get
;;; C-c C-i      twelf-server-interrupt
;;; M-x twelf-server
;;; M-x twelf-server-configure
;;; M-x twelf-server-quit
;;; M-x twelf-server-restart
;;; M-x twelf-server-send-command
;;;
;;; --- Timers ---
;;; M-x twelf-timers-reset
;;; M-x twelf-timers-show
;;; M-x twelf-timers-check
;;;
;;; --- Tags (standard Emacs etags package) ---
;;; M-x twelf-tag
;;; M-.          find-tag (standard binding)
;;; C-x 4 .      find-tag-other-window (standard binding)
;;; C-c q        tags-query-replace (Twelf mode binding)
;;; C-c s        tags-search (Twelf mode binding)
;;; M-,          tags-loop-continue (standard binding)
;;;              visit-tags-table, list-tags, tags-apropos
;;;
;;; --- Communication with inferior Twelf-SML process (not Twelf Server) ---
;;; M-x twelf-sml
;;; C-c C-e      twelf-sml-send-query
;;; C-c C-r      twelf-sml-send-region
;;; C-c RET      twelf-sml-send-newline
;;; C-c ;        twelf-sml-send-semicolon
;;; C-c d        twelf-sml-cd
;;; M-x twelf-sml-quit
;;;
;;; --- Variables ---
;;; twelf-indent        amount of indentation for nested Twelf expressions
;;;
;;;======================================================================
;;; Some Terminology
;;;======================================================================
;;;
;;; Twelf Server --- an inferior process that services requests to type-check,
;;; load, or execute declarations and queries.  It is usually attached to the
;;; buffer *twelf-server*.  Requests are generated by Emacs from user commands,
;;; or may be typed directly into the Twelf server buffer.
;;;
;;; Current configuration --- A configuration is an ordered list of
;;; Twelf source files in dependency order.  It is usually initialized
;;; and maintained in a file sources.cfg.  The current configuration is
;;; also the bases for the TAGS file created by twelf-tags.  This allows
;;; quick jumping to declaration sites for constants, or to apply
;;; searches or replacements to all files in a configuration.
;;;
;;; Current Twelf declaration --- When checking individual declarations
;;; Emacs must extract it from the current buffer and then send it to
;;; the server.  This is necessarily based on a heuristic, since Emacs
;;; does not know enough in order to parse Twelf source properly in all
;;; cases, but it knows the syntax for comments, Twelf identifiers, and
;;; matching delimiters.  Search for the end or beginning of a
;;; declaration is always limited by double blank lines in order to be
;;; more robust (in case a period is missing at the end of a
;;; declaration).  If the point falls between declarations, the
;;; declaration after the point is considered current.
;;;
;;; Twelf-SML --- During development or debugging of the Twelf
;;; implementation itself it is often useful to interact with SML, the
;;; language in which Twelf is implementated, rather than using an Twelf
;;; server.  This is an inferior SML process which may run a Twelf
;;; query interpreter.
;;;
;;;======================================================================
;;; Change Log
;;;======================================================================
;;;
;;; Thu Jun  3 14:51:35 1993 -fp
;;; Added variable display-elf-queries.  If T (default) redisplays Elf
;;; buffer after a query has been sent.  Delays one second after sending
;;; the query which is rather arbitrary.
;;; Wed Jun 30 19:57:58 1993
;;; - Error messages in the format line0.col0-line1.col1 can now be parsed.
;;; - Error from std_in, either interactive or through elf-send-query
;;;   can now be tracked.
;;; - Added simple directory tracking and function elf-cd, bound to C-c d.
;;; - improved filename completion in Elf mode under Lucid Emacs.
;;; - replaced tail recursion in elf-indent-line by a while loop.
;;; - changed elf-input-filter to ignore one character inputs.
;;; - elf-error-marker is now updated on every interactive input or send.
;;; - added commands elf-send-newline, bound to C-c RET
;;;   and elf-send-semicolon, bound to C-c ;.
;;;   These are useful when sending queries from a buffer with examples.
;;; Fri Sep  3 15:02:10 1993
;;; Changed definition of elf-current-paragraph so that it recognizes
;;; individual declarations within a traditional ``paragraph'' (separated
;;; by blank lines).
;;; Fri Oct 22 10:05:08 1993
;;; Changed elf-send-query to ensure that the Elf process expects a query
;;; If the Elf process is at the SML prompt, it starts a top level.
;;; If the Elf process is waiting after printing an answer substitution,
;;; it sends a RET.
;;; This is based on a heuristic analysis of the contents of the Elf buffer.
;;; Fri Dec 16 15:27:14 1994
;;; Changed elf-error-marker to elf-error-pos, since it moved in undesirable
;;; ways in Emacs 19.
;;; Fri Jan  6 09:06:54 1995
;;; Major revision: incorporating elf-server.el and elf-tag.el
;;; Thu Jan 12 14:31:36 1995
;;; Finished major revision (version 2.0)
;;; Sat Jun 13 12:14:34 1998
;;; Renamed to Twelf and incorporated menus from elf-menu.el
;;; Major revision for Twelf 1.2 release
;;; Q: Improve tagging for %keyword declarations?
;;; Thu Jun 25 08:52:41 1998
;;; Finished major revision (version 3.0)
;;; Fri Oct  2 11:06:15 1998
;;; Added NT Emacs bug workaround

(require 'comint)
(require 'easymenu)

;;;----------------------------------------------------------------------
;;; User visible variables
;;;----------------------------------------------------------------------

(defvar twelf-indent 3
  "*Indent for Twelf expressions.")

(defvar twelf-infix-regexp ":\\|\\<->\\>\\|\\<<-\\>\\|\\<=\\>"
  "*Regular expression to match Twelf infix operators.
Match must exclude surrounding whitespace.  This is used for indentation.")

(defvar twelf-server-program "twelf-server"
  "*Default Twelf server program.")

(defvar twelf-info-file "twelf.info"
  "*Default info file for Twelf.")

(defvar twelf-server-display-commands nil
  "*If non-nil, the Twelf server buffer will be displayed after each command.
Normally, the Twelf server buffer is displayed only after some selected
commands or if a command is given a prefix argument.")

(defvar twelf-highlight-range-function 'twelf-highlight-range-zmacs
  "*Function which highlights the range analyzed by the server.
This is called for certain commands which apply to a subterm at point.
You may want to change this for FSF Emacs, XEmacs and/or highlight packages.")

(defvar twelf-focus-function 'twelf-focus-noop
  "*Function which focusses on the current declaration or query.
This is called for certain commands which pick out (a part of) a declaration
or query.  You may want to change this for FSF Emacs, XEmacs and/or highlight
packages.")

(defvar twelf-server-echo-commands t
  "*If nil, Twelf server commands will not be echoed in the Twelf server buffer.")

(defvar twelf-save-silently nil
  "*If non-nil, modified buffers are saved without confirmation
before `twelf-check-config' if they belong to the current configuration.")

(defvar twelf-server-timeout 5
  "*Number of seconds before the server is considered delinquent.
This is unsupported in some versions of Emacs.")

(defvar twelf-sml-program "twelf-sml"
  "*Default Twelf-SML program.")

(defvar twelf-sml-args '()
  "*Arguments to Twelf-SML program.")

(defvar twelf-sml-display-queries t
  "*If nil, the Twelf-SML buffer will not be selected after a query.")

(defvar twelf-mode-hook '()
  "List of hook functions to run when switching to Twelf mode.")

(defvar twelf-server-mode-hook '()
  "List of hook functions to run when switching to Twelf Server mode.")

(defvar twelf-config-mode-hook '()
  "List of hook functions to run when switching to Twelf Config minor mode.")

(defvar twelf-sml-mode-hook '()
  "List of hook functions for Twelf-SML mode.")

(defvar twelf-to-twelf-sml-mode '()
  "List of hook functions for 2Twelf-SML minor mode.")

(defvar twelf-config-mode nil
  "Non-NIL means the Twelf Config minor mode is in effect.")

;;;----------------------------------------------------------------------
;;; Internal variables
;;;----------------------------------------------------------------------

(defvar *twelf-server-buffer-name* "*twelf-server*"
  "The default name for the Twelf server buffer.")

(defvar *twelf-server-buffer* nil
  "The buffer with the Twelf server if one exists.")

(defvar *twelf-server-process-name* "twelf-server"
  "Name of the Twelf server process.")

(defvar *twelf-config-buffer* nil
  "The current Twelf configuration buffer if one exists.")

(defvar *twelf-config-time* nil
  "The modification time of Twelf configuration file when read by the server.")

(defvar *twelf-config-list* nil
  "The reversely ordered list with files in the current Twelf configuration.")

(defvar *twelf-server-last-process-mark* 0
  "The process mark before the last command in the Twelf server buffer.")

(defvar *twelf-last-region-sent* nil
  "Contains a list (BUFFER START END) identifying the last region sent
to the Twelf server or Twelf-SML process for error tracking.
If nil, then the last input was interactive.
If t, then the last input was interactive, but has already been copied
to the end of the Twelf-SML buffer.")

(defvar *twelf-last-input-buffer* nil
  "Last buffer to which input was sent.
This is used by the error message parser.")

(defvar *twelf-error-pos* 0
  "Last error position in the server buffer.")

(defconst *twelf-read-functions*
  '((nat . twelf-read-nat)
    (bool . twelf-read-bool)
    (limit . twelf-read-limit)
    (strategy . twelf-read-strategy))
  "Association between Twelf parameter types and their Emacs read functions.")

(defconst *twelf-parm-table*
  '(("chatter" . nat)
    ("doubleCheck" . bool)
    ("Print.implicit" . bool)
    ("Print.depth" . limit)
    ("Print.length" . limit)
    ("Print.indent" . nat)
    ("Print.width" . nat)
    ("Prover.strategy" . strategy)
    ("Prover.maxSplit" . nat)
    ("Prover.maxRecurse" . nat))
  "Association between Twelf parameters and their types.")

(defvar twelf-chatter 3
  "Chatter level in current Twelf server.
Maintained to present reasonable menus.")

;(defvar twelf-trace 0
;  "Trace level in current Twelf server.
;Maintained to present reasonable menus.")

(defvar twelf-double-check "false"
  "Current value of doubleCheck Twelf parameter.")

(defvar twelf-print-implicit "false"
  "Current value of Print.implicit Twelf parameter.")

(defconst *twelf-track-parms*
  '(("chatter" . twelf-chatter)
    ;("trace" . twelf-trace)
    ("doubleCheck" . twelf-double-check)
    ("Print.implicit" . twelf-print-implicit))
  "Association between Twelf parameters and Emacs tracking variables.")

;;;----------------------------------------------------------------------
;;; Basic key bindings
;;;----------------------------------------------------------------------

(defun install-basic-twelf-keybindings (map)
  "General key bindings for Twelf and Twelf Server modes."
  ;; Additional tag keybindings
  (define-key map "\C-cq" 'tags-query-replace)
  (define-key map "\C-cs" 'tags-search)
  ;; Server state
  (define-key map "\C-c<" 'twelf-set)
  (define-key map "\C-c>" 'twelf-get)
  ;; Error handling
  (define-key map "\C-c`" 'twelf-next-error)
  (define-key map "\C-c=" 'twelf-goto-error)
  ;; Proper indentation
  (define-key map "\e\C-q" 'twelf-indent-decl)
  (define-key map "\t" 'twelf-indent-line)
  (define-key map "\177" 'backward-delete-char-untabify)
  ;; Info documentation
  (define-key map "\C-c\C-h" 'twelf-info)
  )

;;;----------------------------------------------------------------------
;;; Twelf mode
;;; This mode should be used for files with Twelf declarations,
;;; usually *.elf, *.quy, or *.thm, and Twelf configuration files *.cfg
;;;----------------------------------------------------------------------

(defun install-twelf-keybindings (map)
  "Install the key bindings for the Twelf mode."
  (define-key map "\C-cl" 'twelf-font-fontify-buffer) ;autoload twelf-font
  (define-key map "\C-c\C-l" 'twelf-font-fontify-decl) ;autoload twelf-font
  (define-key map "\C-c\C-i" 'twelf-server-interrupt)
  (define-key map "\C-c\C-u" 'twelf-server-display)
  (define-key map "\C-cc" 'twelf-type-const)
  ;(define-key map "\C-ce" 'twelf-expected-type-at-point)
  ;(define-key map "\C-cp" 'twelf-type-at-point)
  ;(define-key map "\C-c." 'twelf-complete)
  ;(define-key map "\C-c?" 'twelf-completions-at-point)
  (define-key map "\C-c\C-d" 'twelf-check-declaration)
  (define-key map "\C-c\C-s" 'twelf-save-check-file)
  (define-key map "\C-c\C-c" 'twelf-save-check-config)
  )

(defvar twelf-mode-map nil
  "The keymap used in Twelf mode.")

(cond ((not twelf-mode-map)
       (setq twelf-mode-map (make-sparse-keymap))
       (install-basic-twelf-keybindings twelf-mode-map)
       (install-twelf-keybindings twelf-mode-map)))

;;;----------------------------------------------------------------------
;;; General editing and indentation
;;;----------------------------------------------------------------------

(defvar twelf-mode-syntax-table nil
  "The syntax table used in Twelf mode.")

(defun set-twelf-syntax (char entry)
  (modify-syntax-entry char entry twelf-mode-syntax-table))
(defun set-word (char) (set-twelf-syntax char "w   "))
(defun set-symbol (char) (set-twelf-syntax char "_   "))

(defun map-string (func string)
  (if (string= "" string)
      ()
    (funcall func (string-to-char string))
    (map-string func (substring string 1))))

(if twelf-mode-syntax-table
    ()
  (setq twelf-mode-syntax-table (make-syntax-table))
  ;; A-Z and a-z are already word constituents
  ;; For fontification, it would be better if _ and ' were word constituents
  (map-string 'set-word "!&$^+/<=>?@~|#*`;,-0123456789\\") ; word constituents
  (map-string 'set-symbol "_'")         ; symbol constituents
  ;; Delimited comments are %{ }%, see 1234 below.
  (set-twelf-syntax ?\ "    ")            ; whitespace
  (set-twelf-syntax ?\t "    ")           ; whitespace
  (set-twelf-syntax ?% "< 14")            ; comment begin
  (set-twelf-syntax ?\n ">   ")           ; comment end
  (set-twelf-syntax ?: ".   ")            ; punctuation
  (set-twelf-syntax ?. ".   ")            ; punctuation
  (set-twelf-syntax ?\( "()  ")           ; open delimiter
  (set-twelf-syntax ?\) ")(  ")           ; close delimiter
  (set-twelf-syntax ?\[ "(]  ")           ; open delimiter
  (set-twelf-syntax ?\] ")[  ")           ; close delimiter
  (set-twelf-syntax ?\{ "(}2 ")           ; open delimiter
  (set-twelf-syntax ?\} "){ 3")           ; close delimiter
  ;; Actually, strings are illegal but we include:
  (set-twelf-syntax ?\" "\"   ")          ; string quote
  ;; \ is not an escape, but a word constituent (see above)
  ;;(set-twelf-syntax ?\\ "/   ")         ; escape
  )

(defconst *whitespace* " \t\n\f"
  "Whitespace characters to be skipped by various operations.")

(defconst *twelf-comment-start* (concat "%[%{" *whitespace* "]")
  "Regular expression to match the start of a Twelf comment.")

(defconst *twelf-id-chars* "a-z!&$^+/<=>?@~|#*`;,\\-\\\\A-Z_0-9'"
  "Characters that constitute Twelf identifiers.")

(defun skip-twelf-comments-and-whitespace ()
  "Skip Twelf comments (single-line or balanced delimited) and white space."
  (skip-chars-forward *whitespace*)
  (while (looking-at *twelf-comment-start*)
    (cond ((looking-at "%{")		; delimited comment
	   (condition-case nil (forward-sexp 1)
	     (error (goto-char (point-max))))
	   (or (eobp) (forward-char 1)))
	  (t				; single-line comment
	   (end-of-line 1)))
    (skip-chars-forward *whitespace*)))

(defun twelf-end-of-par (&optional limit)
  "Skip to presumed end of current Twelf declaration.
Moves to next period or blank line (whichever comes first)
and returns t if period is found, nil otherwise.
Skips over comments (single-line or balanced delimited).
Optional argument LIMIT specifies limit of search for period."
  (if (not limit)
      (save-excursion
	(forward-paragraph 1)
	(setq limit (point))))
  (while (and (not (looking-at "\\."))
	      (< (point) limit))
    (skip-chars-forward "^.%" limit)
    (cond ((looking-at *twelf-comment-start*)
	   (skip-twelf-comments-and-whitespace))
	  ((looking-at "%")
	   (forward-char 1))))
  (cond ((looking-at "\\.")
	 (forward-char 1)
	 t)
	(t ;; stopped at limit
	 nil)))

(defun twelf-current-decl ()
  "Returns list (START END COMPLETE) for current Twelf declaration.
This should be the declaration or query under or just before
point within the nearest enclosing blank lines.
If declaration ends in `.' then COMPLETE is t, otherwise nil."
  (let (par-start par-end complete)
    (save-excursion
      ;; Skip backwards if between declarations
      (if (or (eobp) (looking-at (concat "[" *whitespace* "]")))
	  (skip-chars-backward (concat *whitespace* ".")))
      (setq par-end (point))
      ;; Move forward from beginning of decl until last
      ;; declaration before par-end is found.
      (if (not (bobp)) (backward-paragraph 1))
      (setq par-start (point))
      (while (and (twelf-end-of-par par-end)
		  (< (point) par-end))
	(setq par-start (point)))
      ;; Now par-start is at end of preceding declaration or query.
      (goto-char par-start)
      (skip-twelf-comments-and-whitespace)
      (setq par-start (point))
      ;; Skip to period or consective blank lines
      (setq complete (twelf-end-of-par))
      (setq par-end (point)))
    (list par-start par-end complete)))

(defun twelf-mark-decl ()
  "Marks current Twelf declaration and moves point to its beginning."
  (interactive)
  (let* ((par (twelf-current-decl))
	 (par-start (nth 0 par))
	 (par-end (nth 1 par)))
    (push-mark par-end)
    (goto-char par-start)))

(defun twelf-indent-decl ()
  "Indent each line of the current Twelf declaration."
  (interactive)
  (let* ((par (twelf-current-decl))
	 (par-start (nth 0 par))
	 (par-end (nth 1 par)))
    (goto-char par-start)
    (twelf-indent-lines (count-lines par-start par-end))))

(defun twelf-indent-region (from to)
  "Indent each line of the region as Twelf code."
  (interactive "r")
  (cond ((< from to)
	 (goto-char from)
	 (twelf-indent-lines (count-lines from to)))
	((> from to)
	 (goto-char to)
	 (twelf-indent-lines (count-lines to from)))
	(t nil)))

(defun twelf-indent-lines (n)
  "Indent N lines starting at point."
  (interactive "p")
  (while (> n 0)
    (twelf-indent-line)
    (forward-line 1)
    (setq n (1- n))))

(defun twelf-comment-indent ()
  "Calculates the proper Twelf comment column.
Currently does not deal specially with pragmas."
  (cond ((looking-at "%%%")
	 0)
	((looking-at "%[%{]")
	 (car (twelf-calculate-indent)))
	(t
	 (skip-chars-backward " \t")
	 (max (if (bolp) 0 (1+ (current-column))) comment-column))))

(defun looked-at ()
  "Returns the last string matched against.
Beware of intervening, even unsuccessful matches."
  (buffer-substring (match-beginning 0) (match-end 0)))

(defun twelf-indent-line ()
  "Indent current line as Twelf code.
This recognizes comments, matching delimiters, and standard infix operators."
  (interactive)
  (let ((old-point (point)))
    (beginning-of-line)
    (let* ((indent-info (twelf-calculate-indent))
	   (indent-column (nth 0 indent-info))
	   (indent-type (nth 1 indent-info))
	   (indent-string (nth 2 indent-info)))
      (skip-chars-forward " \t")        ; skip whitespace
      (let ((fwdskip (- old-point (point))))
	(cond ((looking-at "%%%")
	       (twelf-indent-line-to 0 fwdskip)) ; %%% comment at column 0
	      ((looking-at "%[%{]")     ; delimited or %% comment
	       (twelf-indent-line-to indent-column fwdskip))
	      ((looking-at *twelf-comment-start*)    ; indent single-line comment
	       (indent-for-comment)
	       (forward-char -1))
	      ((looking-at "%")		; %keyword declaration
	       (twelf-indent-line-to indent-column fwdskip))
	      ((looking-at twelf-infix-regexp) ; looking at infix operator
	       (if (string= indent-string (looked-at))
		   ;; indent string is the same as the one we are looking at
		   (twelf-indent-line-to indent-column fwdskip)
		 (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))
	      ((eq indent-type 'delimiter) ; indent after delimiter
	       (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip))
	      ((eq indent-type 'limit)  ; no delimiter or infix found.
	       (twelf-indent-line-to indent-column fwdskip))
	      ((eq indent-type 'infix)
	       (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))))))

(defun twelf-indent-line-to (indent fwdskip)
  "Indent current line to INDENT then skipping to FWDSKIP if positive.
Assumes point is on the first non-whitespace character of the line."
  (let ((text-start (point))
	(shift-amount (- indent (current-column))))
    (if (= shift-amount 0)
	nil
      (beginning-of-line)
      (delete-region (point) text-start)
      (indent-to indent))
    (if (> fwdskip 0)
	(forward-char fwdskip))))

(defun twelf-calculate-indent ()
  "Calculate the indentation and return a list (INDENT INDENT-TYPE STRING).
INDENT is a natural number,
INDENT-TYPE is 'DELIMITER, 'INFIX, or 'LIMIT, and
STRING is the delimiter, infix operator, or the empty string, respectively."
  (save-excursion
    (let* ((par (twelf-current-decl))
	   (par-start (nth 0 par))
	   (par-end (nth 1 par))
	   (par-complete (nth 2 par))
	   (limit (cond ((> par-start (point)) (point))
			((and (> (point) par-end) par-complete) par-end)
			(t par-start))))
      (twelf-dsb limit))))

(defun twelf-dsb (limit)
  "Scan backwards from point to find opening delimiter or infix operator.
This currently does not deal with comments or mis-matched delimiters.
Argument LIMIT specifies bound for backwards search."
  (let ((result nil)
	(lparens 0) (lbraces 0) (lbrackets 0))
    (while (not result)
      (if (or (= lparens 1) (= lbraces 1) (= lbrackets 1))
	  (setq result (list (current-column) 'delimiter (looked-at)))
	(if (re-search-backward (concat "[][{}()]\\|" twelf-infix-regexp)
				limit 'limit) ; return 'LIMIT if limit reached
	    (let ((found (looked-at)))
	      (cond
	       ((string= found "(") (setq lparens (1+ lparens)))
	       ((string= found ")") (setq lparens (1- lparens)))
	       ((string= found "{") (setq lbraces (1+ lbraces)))
	       ((string= found "}") (setq lbraces (1- lbraces)))
	       ((string= found "[") (setq lbrackets (1+ lbrackets)))
	       ((string= found "]") (setq lbrackets (1- lbrackets)))
	       (t;; otherwise, we are looking at an infix operator
		(if (and (= lparens 0) (= lbraces 0) (= lbrackets 0))
		    (setq result (list (current-column) 'infix found))
		  nil))))               ; embedded - skip
	  (setq result (list 0 'limit ""))))) ; reached the limit, no indent
    result))

(defun twelf-mode-variables ()
  "Set up local variables for Twelf mode."
  (set-syntax-table twelf-mode-syntax-table)
  ;; Paragraphs are separated by blank lines or ^L.
  (make-local-variable 'paragraph-start)
  (setq paragraph-start "^[ \t\f]*$")
  (make-local-variable 'paragraph-separate)
  (setq paragraph-separate paragraph-start)
  (make-local-variable 'indent-line-function)
  (setq indent-line-function 'twelf-indent-line)
  (make-local-variable 'comment-start)
  (setq comment-start "%")
  (make-local-variable 'comment-start-skip)
  (setq comment-start-skip "%+{?[ \t]*")
  (make-local-variable 'comment-end)
  (setq comment-end "")
  (make-local-variable 'comment-column)
  (setq comment-column 40)
  ;; (make-local-variable 'parse-sexp-ignore-comments)
  ;; (setq parse-sexp-ignore-comments t)
  )

(defun twelf-mode ()
  "Major mode for editing Twelf code.
Tab indents for Twelf code.
Delete converts tabs to spaces as it moves back.
M-C-q indents all lines in current Twelf declaration.

Twelf mode also provides commands to maintain groups of Twelf source
files (configurations) and communicate with an Twelf server which
processes declarations.  It also supports quick jumps to the (presumed)
source of error message that may arise during parsing or type-checking.

Customisation: Entry to this mode runs the hooks on twelf-mode-hook.
See also the hints for the .emacs file given below.

Mode map
========
\\{twelf-mode-map}
\\<twelf-mode-map>
Overview
========

The basic architecture is that Emacs sends commands to an Twelf server
which runs as an inferior process, usually in the buffer *twelf-server*.
Emacs in turn interprets or displays the replies from the Twelf server.
Since a typical Twelf application comprises several files, Emacs
maintains a configuration in a file, usally called sources.cfg.  This
file contains a list of files, each on a separate line, in dependency
order.  The `%' character starts a comment line.  A configuration is
established with the command \\[twelf-server-configure].

A new file is switched to Twelf mode if a file has extension `.elf',
`.quy', `.thm' or `.cfg' and the `auto-mode-alist' is set correctly (see
init.el).

The files in the current configuration can be checked in sequence with
\\[twelf-save-check-config], the current file with
\\[twelf-save-check-file], individual declarations with
\\[twelf-check-declaration].  These, like many other commands, take an
optional prefix arguments which means to display the Twelf server buffer
after the processing of the configuration, file, or declaration.  If an
error should arise during these or related operations a message is
issued both in the server buffer and Emacs, and the command
\\[twelf-next-error] visits the presumed source of the type error in a
separate buffer.

Summary of most common commands:
 M-x twelf-save-check-config \\[twelf-save-check-config]  save, check & load configuration
 M-x twelf-save-check-file   \\[twelf-save-check-file]  save, check & load current file
 M-x twelf-check-declaration \\[twelf-check-declaration]  type-check declaration at point
 M-x twelf-server-display    \\[twelf-server-display]  display Twelf server buffer

It is important to remember that the commands to save and check
a file or check a declaration may change the state of the global
signature maintained in Twelf.  After a number of changes it is usually
a good idea to return to a clean slate with \\[twelf-save-check-config].

Individual Commands
===================

Configurations, Files and Declarations

  twelf-save-check-config                   \\[twelf-save-check-config]
   Save its modified buffers and then check the current Twelf configuration.
   With prefix argument also displays Twelf server buffer.
   If necessary, this will start up an Twelf server process.

  twelf-save-check-file                     \\[twelf-save-check-file]
   Save buffer and then check it by giving a command to the Twelf server.
   With prefix argument also displays Twelf server buffer.

  twelf-check-declaration                   \\[twelf-check-declaration]
   Send the current declaration to the Twelf server process for checking.
   With prefix argument, subsequently display Twelf server buffer.

Subterm at Point

  twelf-type-const                          \\[twelf-type-const]
   Display the type of the constant before point.
   Note that the type of the constant will be `absolute' rather than the
   type of the particular instance of the constant.

Error Tracking

  twelf-next-error                          \\[twelf-next-error]
   Find the next error by parsing the Twelf server or Twelf-SML buffer.

  twelf-goto-error                          \\[twelf-goto-error]
   Go to the error reported on the current line or below.

Server State

  twelf-set PARM VALUE                      \\[twelf-set]
   Sets the Twelf server parameter PARM to VALUE.
   Prompts for PARM when called interactively, using completion for legal
   parameters.

  twelf-get PARM                            \\[twelf-get]
   Print the current value the Twelf server parameter PARM.

  twelf-server-interrupt                    \\[twelf-server-interrupt]
   Interrupt the Twelf server-process.

  twelf-server                              \\[twelf-server]
   Start a Twelf server process in a buffer named *twelf-server*.

  twelf-server-configure                    \\[twelf-server-configure]
   Set the current configuration of the Twelf server.

  twelf-reset                               \\[twelf-reset]
   Reset the global signature in the Twelf server process.

  twelf-server-quit                         \\[twelf-server-quit]
   Kill the Twelf server process.

  twelf-server-restart                      \\[twelf-server-restart]
   Restarts server and re-initializes configuration.
   This is primarily useful during debugging of the Twelf server code or
   if the Twelf server is hopelessly wedged.

  twelf-server-send-command                 \\[twelf-server-send-command]
   Send arbitrary string to Twelf server.

Tags (for other, M-x apropos tags or see `etags' documentation)

  twelf-tag                                 \\[twelf-tag]
   Create tags file TAGS for current configuration.
   If current configuration is names CONFIGx, tags file will be named TAGx.
   Errors are displayed in the Twelf server buffer.

Timers

  twelf-timers-reset			    \\[twelf-timers-reset]
   Reset Twelf timers.

  twelf-timers-show                         \\[twelf-timers-show]
   Show and reset Twelf timers.

  twelf-timers-check                        \\[twelf-timers-check]
   Show, but do not reset Twelf timers.

Editing

  twelf-indent-decl                         \\[twelf-indent-decl]
   Indent each line in current declaration as Twelf code.

  twelf-indent-region                       \\[twelf-indent-region]
   Indent each line of the region as Twelf code.

Minor Modes
===========

An associated minor modes is 2Twelf-SML (toggled with
twelf-to-twelf-sml-mode).  This means that we assume communication
is an inferior Twelf-SML process and not a Twelf server.

Related Major Modes
===================

Related major modes are Twelf Server (for the Twelf server buffer) and
Twelf-SML (for an inferior Twelf-SML process).  Both modes are based on
the standard Emacs comint package and inherit keybindings for retrieving
preceding input.

Customization
=============

The following variables may be of general utility.

 twelf-indent          amount of indentation for nested Twelf expressions
 twelf-mode-hook       hook to run when entering Twelf mode
 twelf-server-program  full pathname of Twelf server program
 twelf-server-mode-hook  hook to run when entering Twelf server mode
 twelf-info-file       name of Twelf info file with documentation

The following is a typical section of a .emacs initialization file
which can be found in the file init.el.

(setq load-path (cons \"/afs/cs/project/twelf/research/twelf/emacs\" load-path))

(autoload 'twelf-mode \"twelf\" \"Major mode for editing Twelf source.\" t)
(autoload 'twelf-server \"twelf\" \"Run an inferior Twelf server.\" t)
(autoload 'twelf-sml \"twelf\" \"Run an inferior Twelf-SML process.\" t)

(setq auto-mode-alist
      (cons '(\"\\.elf$\" . twelf-mode)
	    (cons '(\"\\.quy$\" . twelf-mode)
		  (cons '(\"\\.thm$\" . twelf-mode)
			(cons '(\"\\.cfg$\" . twelf-mode)
			      auto-mode-alist)))))

(setq twelf-server-program
      \"/afs/cs/project/twelf/research/twelf/bin/twelf-server\")

(setq twelf-sml-program
      \"/afs/cs/project/twelf/misc/smlnj/bin/sml-cm\")

(setq twelf-info-file
      \"/afs/cs/project/twelf/research/twelf/doc/info/twelf.info\")
"
  (interactive)
  (kill-all-local-variables)
  (twelf-mode-variables)
  (use-local-map twelf-mode-map)
  (setq major-mode 'twelf-mode)
  (setq mode-name "Twelf")
  (twelf-config-mode-check)
  (twelf-add-menu)			; add Twelf menu to menubar
  ;; disable twelf-add-to-config-check: require explicit add-file
  ;; (twelf-add-to-config-check)
  (run-hooks 'twelf-mode-hook))

;;;----------------------------------------------------------------------
;;; Reading info file
;;;----------------------------------------------------------------------

(defun twelf-info (&optional file)
  "Enter Info, starting with the Twelf node
Optional argument FILE specifies the info file.

In interactive use, a prefix arguments directs this command to
read a file name from the minibuffer."
  (interactive (if current-prefix-arg
		   (list (read-file-name "Info file name: " nil nil t))))
  (info (or file twelf-info-file)))

;;;----------------------------------------------------------------------
;;; Error message parsing
;;;----------------------------------------------------------------------

(defconst twelf-error-regexp
  "^.+:[-0-9.:]+.* \\(Error\\|Warning\\):"
  "Regexp for matching Twelf error.")

(defconst twelf-error-fields-regexp
   "^[-=? \t]*\\(.+\\):\
\\([0-9]+\\)\\(\\.\\([0-9]+\\)\\)?\\(-\\([0-9]+\\)\\(\\.\\([0-9]+\\)\\)?\\)?\
.+\\(Error\\|Warning\\):"
   "Regexp to extract fields of Twelf error.")

(defconst twelf-error-decl-regexp
  "^[-=? \t]*\\(.+\\)::\\([^ \t\n]+\\) "
  "Regexp to extract filename and identifier from declaration error.")

(defun looked-at-nth (n)
  (let ((b (match-beginning n))
	(e (match-end n)))
    (if (or (null b) (null e)) nil
      (buffer-substring (match-beginning n) (match-end n)))))

(defun looked-at-nth-int (n)
  (let ((str (looked-at-nth n)))
    (if (null str) nil
      (string-to-number str))))

(defun twelf-error-parser (pt)
  "Standard parser for Twelf errors.
Returns a 5-element list (FILE START-LINE START-COL END-LINE END-COL)
or (\"Local\" START-CHAR NIL END-CHAR NIL)."
  (save-excursion
    (goto-char pt)
    (re-search-forward twelf-error-fields-regexp)
    (list (looked-at-nth 1)		; file or "Local" or "stdIn"
	  (looked-at-nth-int 2)		; start line or char
	  (looked-at-nth-int 4)		; start column, if given, else nil
	  (looked-at-nth-int 6)		; end line, if given, else nil or char
	  (looked-at-nth-int 8)		; end column, if given, else nil
	  )))

(defun twelf-error-decl (pos)
  "Determines if the error is identified only by its declaration."
  (save-excursion
    (goto-char pos)
    (looking-at twelf-error-decl-regexp)))

(defun twelf-mark-relative (line0 col0 line1 col1)
  "Mark error region if location is given relative to a buffer position."
  (if (not (= line0 1))
      (forward-line (1- line0)))
  ;; work around bug: from stdIn, first line is off by one.
  (forward-char (if (not (= line0 1)) (1- col0) (1- (1- col0))))
  ;; select region, if non-empty
  (cond ((not (null line1))
	 (push-mark (point))
	 (cond ((not (= line1 line0))
		(forward-line (- line1 line0))
		(forward-char (1- col1)))
	       (t (forward-char (- col1 col0))))
	 (exchange-point-and-mark)
	 (funcall twelf-highlight-range-function (point) (mark)))))

(defun twelf-mark-absolute (line0 col0 line1 col1)
  "Mark error region if location is given as absolute buffer position."
  (cond ((and line0 col0 line1 col1)	; line0.col0-line1.col1 range
	 (goto-line line0)
	 ;; don't use move-to-column since <tab> is 1 char to lexer
	 (forward-char (1- col0))
	 ;; select region, if non-empty
	 (push-mark (point))
	 (goto-line line1)
	 (forward-char (1- col1))
	 (exchange-point-and-mark)
	 (funcall twelf-highlight-range-function (point) (mark)))
	((and (null col0) (null col1))	; char0-char1 range
	 (goto-char line0)
	 (push-mark (point))
	 (goto-char line1)
	 (exchange-point-and-mark)
	 (funcall twelf-highlight-range-function (point) (mark)))
	((and line0 col0)		; beginning line0.col0
	 (goto-line line0)
	 (forward-char (1- col0)))
	(line0				; beginning char0
	 (goto-char line0))
	(t (error "Unrecognized format for error location"))))

(defun twelf-find-decl (filename id)
  "In FILENAME find probable declaration of ID."
  (if (not (file-readable-p filename))
      (error "Cannot read file %s" filename)
    (switch-to-buffer-other-window (find-file-noselect filename))
    (goto-char (point-min))
    (let ((done nil)
	  decl-id)
      (while (not done)
	(setq decl-id (twelf-next-decl filename *twelf-last-input-buffer*))
	(if (not decl-id)
	    (error "Declaration of %s not found in file %s." id filename)
	  (setq done (string= decl-id id))
	  (if (not done) (twelf-end-of-par)))))))

(defun twelf-next-error ()
  "Find the next error by parsing the Twelf server or Twelf-SML buffer.
Move the error message on the top line of the window;
put the cursor at the beginning of the error source. If the
error message specifies a range, the mark is placed at the end."
  (interactive)
  (let ((case-fold-search nil)
	(twelf-buffer (or *twelf-last-input-buffer*
			(error "Cannot determine process buffer with last input")))
	error-begin)
    (pop-to-buffer twelf-buffer)
    (goto-char *twelf-error-pos*)   ; go to last error
    (if (not (re-search-forward twelf-error-regexp (point-max) t))
	(error "No error message found.")
      (setq error-begin (match-beginning 0))
      (setq *twelf-error-pos* (point))
      (set-window-start (get-buffer-window twelf-buffer)
			(save-excursion (beginning-of-line) (point)))
      (if (twelf-error-decl error-begin)
	  (twelf-find-decl (looked-at-nth 1) (looked-at-nth 2))
	(let* ((parse (twelf-error-parser error-begin))
	       (file (nth 0 parse))
	       (line0 (nth 1 parse))
	       (col0 (nth 2 parse))
	       (line1 (nth 3 parse))
	       (col1 (nth 4 parse)))
	  (cond ((equal file "stdIn")
		 ;; Error came from direct input
		 (cond ((null *twelf-last-region-sent*)
			;; from last interactive input in the Twelf buffer
			(goto-char (point-max))
			(comint-previous-input 1)
			(setq *twelf-last-region-sent* t)
			(goto-char (process-mark
				    (get-buffer-process twelf-buffer)))
			(twelf-mark-relative line0 col0 line1 col1))
		       ((eq *twelf-last-region-sent* t)
			;; from the waiting input in the Twelf buffer
			(goto-char (process-mark
				    (get-buffer-process twelf-buffer)))
			(twelf-mark-relative line0 col0 line1 col1))
		       (t
			;; from a region sent from some buffer
			(let ((buf (nth 0 *twelf-last-region-sent*))
			      (start (nth 1 *twelf-last-region-sent*)))
			  (switch-to-buffer-other-window buf)
			  (goto-char start)
			  (twelf-mark-relative line0 col0 line1 col1)))))
		((equal file "Local")
		 ;; Error came from local input, usually to a server process
		 ;; in this case the address relative, and expressed in
		 ;; characters, rather than lines.
		 (let ((local-buffer (nth 0 *twelf-last-region-sent*))
		       ;; Local characters seem to be off by two
		       (char0 (+ (nth 1 *twelf-last-region-sent*) (- line0 2)))
		       (char1 (+ (nth 1 *twelf-last-region-sent*) (- line1 2))))
		   (switch-to-buffer-other-window local-buffer)
		   (goto-char char1)
		   (push-mark)
		   (goto-char char0)
		   (exchange-point-and-mark)))
		((file-readable-p file)
		 ;; Error came from a source file
		 (switch-to-buffer-other-window (find-file-noselect file))
		 (twelf-mark-absolute line0 col0 line1 col1))
		(t
		 (error (concat "Can't read file " file)))))))))

(defun twelf-goto-error ()
  "Go to the error reported on the current line or below.
Also updates the error cursor to the current line."
  (interactive)
  (pop-to-buffer (or *twelf-last-input-buffer*
		     (error "Cannot determine process buffer with last input")))
  (beginning-of-line)
  (setq *twelf-error-pos* (point))
  (twelf-next-error))

;;;----------------------------------------------------------------------
;;; NT Emacs bug workaround
;;;----------------------------------------------------------------------

(defun twelf-convert-standard-filename (filename)
  "Convert FILENAME to form appropriate for Twelf Server of current OS."
  (cond ((eq system-type 'windows-nt)
	 (while (string-match "/" filename)
	   (setq filename (replace-match "\\" t t filename)))
	 filename)
	(t (convert-standard-filename filename))))

;;;----------------------------------------------------------------------
;;; Communication with Twelf server
;;;----------------------------------------------------------------------

(defun string-member (x l)
  (if (null l) nil
    (or (string-equal x (car l)) (string-member x (cdr l)))))

;(defun twelf-add-to-config-check ()
;  "Ask if current file should be added to the current Twelf configuration."
;  (let ((file-name (buffer-file-name)))
;    (if (and (not (string-member file-name *twelf-config-list*))
;             (not (null *twelf-config-buffer*))
;             (yes-or-no-p "Add to the current configuration? "))
;        (twelf-server-add-file file-name))))

(defun twelf-config-proceed-p (file-name)
  "Ask if to proceed if FILE-NAME is not in current configuration."
  (if (and (not (string-member file-name *twelf-config-list*))
	   (not (yes-or-no-p "File not in current configuration.  Save? ")))
      nil
    t))

(defun twelf-save-if-config (buffer)
  "Ask if BUFFER should be saved if in the current configuration.
Always save if the variable `twelf-save-silently' is non-nil."
  (let ((file-name (buffer-file-name buffer)))
    (if (and (buffer-modified-p buffer)
	     file-name
	     (string-member file-name *twelf-config-list*))
	(if twelf-save-silently
	    (save-buffer)
	  (pop-to-buffer buffer)
	  (if (yes-or-no-p (concat "Save " file-name "? "))
	      (save-buffer))))))

(defun twelf-config-save-some-buffers ()
  "Cycle through all buffers and save those in the current configuration."
  (mapcar 'twelf-save-if-config (buffer-list)))

(defun twelf-save-check-config (&optional displayp)
  "Save its modified buffers and then check the current Twelf configuration.
With prefix argument also displays Twelf server buffer.
If necessary, this will start up an Twelf server process."
  (interactive "P")
  (let ((current-file-name (buffer-file-name)))
    (cond ((and current-file-name
		(not buffer-read-only)
		(buffer-modified-p)
		(twelf-config-proceed-p current-file-name))
	   (save-buffer)))
    (save-excursion
      (twelf-config-save-some-buffers))
    (twelf-check-config displayp)))

(defun twelf-check-config (&optional displayp)
  "Check the current Twelf configuration.
With prefix argument also displays Twelf server buffer.
If necessary, this will start up an Twelf server process."
  (interactive "P")
  (if (not *twelf-config-buffer*)
      (call-interactively 'twelf-server-configure))
  (twelf-server-sync-config)
  (twelf-focus nil nil)
  (twelf-server-send-command "Config.load")
  (twelf-server-wait displayp))

(defun twelf-save-check-file (&optional displayp)
  "Save buffer and then check it by giving a command to the Twelf server.
In Twelf Config minor mode, it reconfigures the server.
With prefix argument also displays Twelf server buffer."
  (interactive "P")
  (save-buffer)
  (if twelf-config-mode
      (twelf-server-configure (buffer-file-name) "Server OK: Reconfigured")
    (let* ((save-file (buffer-file-name))
	   (check-file (file-relative-name save-file (twelf-config-directory)))
	   (check-file-os (twelf-convert-standard-filename check-file)))
      (twelf-server-sync-config)
      (twelf-focus nil nil)
      (twelf-server-send-command (concat "loadFile " check-file-os))
      (twelf-server-wait displayp))))

(defun twelf-buffer-substring (start end)
  "The substring of the current buffer between START and END.
The location is recorded for purposes of error parsing."
  (setq *twelf-last-region-sent* (list (current-buffer) start end))
  (buffer-substring start end))

(defun twelf-buffer-substring-dot (start end)
  "The substring of the current buffer between START and END plus
an end-of-input marker, `%.'.  The location of the input is recorded
for purposes of error parsing."
  (concat (twelf-buffer-substring start end) "%."))

(defun twelf-check-declaration (&optional displayp)
  "Send the current declaration to the Twelf server process for checking.
With prefix argument also displays Twelf server buffer."
  (interactive "P")
  (let* ((par (twelf-current-decl))
	 (par-start (nth 0 par))
	 (par-end (nth 1 par))
	 (decl (twelf-buffer-substring-dot par-start par-end)))
    (twelf-focus par-start par-end)
    (twelf-server-send-command (concat "readDecl\n" decl))
    (twelf-server-wait displayp)))

;(defun twelf-highlight-range (par-start par-end &optional offset)
;  "Set point and mark to encompass the range analyzed by the Twelf server."
;  (let* ((range (twelf-parse-range))
;         (range-start (nth 0 range))
;         (range-end (nth 1 range))
;         (offset (if (null offset) 0 offset)))
;    (if (and (integerp range-start) (integerp range-end))
;        (progn (goto-char (+ (- (+ par-start range-end) 2) offset))
;               (push-mark (- (+ par-start range-start) 2))
;	       (funcall twelf-highlight-range-function (point) (mark))))))

(defun twelf-highlight-range-zmacs (start end)
  "Highlight range as zmacs region.  Assumes point and mark are set.
Does nothing if function zmacs-activate-region is undefined."
  (if (fboundp 'zmacs-activate-region)
      (zmacs-activate-region)))

(defun twelf-focus (&optional start end)
  "Focus on region between START and END as current declaration or query.  If
START and END are nil, then no focus exists.  This intermediary just calls
the appropriate function."
  (funcall twelf-focus-function start end))

(defun twelf-focus-noop (start end)
  "This default focus function does nothing."
  ())

;; Not yet available in Twelf 1.2 -fp

;(defun twelf-type-at-point ()
;  "Display the type of the subterm at the point in the current Twelf decl.

;The subterm at point is the smallest subterm whose printed representation
;begins to the left of point and extends up to or beyond point.  After this and
;similar commands applicable to subterms, the current region (between mark and
;point) is set to encompass precisely the selected subterm.  In XEmacs,
;it will thus be highlighted under many circumstances.  In other versions
;of Emacs \\[exchange-point-and-mark] will indicate the extent of the region.

;The type computed for the subterm at point takes contextual information into
;account.  For example, if the subterm at point is a constant with implicit
;arguments, the type displayed will be the instance of the constant (unlike
;M-x twelf-type-const (\\[twelf-type-const]), which yields the absolute type of a constant)."

;  (interactive)
;  (let* ((par (twelf-current-decl))
;         (par-start (nth 0 par))
;         (par-end (nth 1 par))
;         (decl (twelf-buffer-substring-dot par-start par-end)))
;    (twelf-focus par-start par-end)
;    (twelf-server-send-command
;     (concat "type-at "
;             (twelf-current-syncat) " "
;             (int-to-string (+ (- (point) par-start) 2)) "\n"
;             decl))
;    (twelf-server-wait t)
;    (twelf-highlight-range par-start par-end)))

;(defun twelf-expected-type-at-point ()
;  "Display the type expected at the point in the current declaration.

;This replaces the subterm at point by an underscore _ and determines
;the type that _ would have to have for the whole declaration to be valid.
;This is useful for debugging in places where inconsistent type constraints
;have arisen.  Error messages may be given, but will not be correctly
;interpreted by Emacs, since the string sent to the server may be different
;from the declaration in the buffer.

;For a definition of the subterm at point, see function twelf-type-at-point."
;  (interactive)
;  (let* ((par (twelf-current-decl))
;         (par-start (nth 0 par))
;         (par-end (nth 1 par))
;         (par-initial-end nil)
;         (par-final-start nil)
;         modified-decl)
;    ;; (exp-present (not (looking-at (concat "[" *whitespace* "]"))))
;    (backward-sexp 1)
;    (setq par-initial-end (point))
;    (forward-sexp 1)
;    (setq par-final-start (point))
;    (setq modified-decl
;          (concat (twelf-buffer-substring par-start par-initial-end)
;                  "_" (twelf-buffer-substring-dot par-final-start par-end)))
;    ;; Error messages here are not accurate.  Nontheless:
;    (setq *twelf-last-region-sent* (list (current-buffer) par-start par-end))
;    (twelf-focus par-start par-end)
;    (twelf-server-send-command
;     (concat "type-at "
;             (twelf-current-syncat) " "
;             (int-to-string (1+ (+ (- par-initial-end par-start) 2))) "\n"
;             modified-decl))
;    (twelf-server-wait t)
;    (twelf-highlight-range par-start par-end
;			 (1- (- par-final-start par-initial-end)))))

;(defun twelf-parse-range ()
;  "Parse a range as returned by the Twelf server and return as a list."
;  (save-window-excursion
;    (let ((twelf-server-buffer (twelf-get-server-buffer)))
;      (set-buffer twelf-server-buffer)
;      (goto-char *twelf-server-last-process-mark*)
;      ;; We are now at the beginning of the output
;      (re-search-forward "^\\[\\([0-9]+\\),\\([0-9]+\\))")
;      (list (looked-at-nth-int 1) (looked-at-nth-int 2)))))

(defun twelf-type-const ()
  "Display the type of the constant before point.
Note that the type of the constant will be `absolute' rather than the
type of the particular instance of the constant."
  (interactive)
  (let ((previous-point (point)))
    (skip-chars-backward *whitespace* (point-min))
    (skip-chars-forward *twelf-id-chars* (point-max))
    (let ((end-of-id (point)))
      (skip-chars-backward *twelf-id-chars* (point-min))
      (let ((c (if (= (point) end-of-id)
		   ;; we didn't move.  this should eventually become a
		   ;; completing-read
		   (read-string "Constant: ")
		 (buffer-substring (point) end-of-id))))
	(twelf-server-send-command (concat "decl " c))
	(twelf-server-wait t)             ; Wait for and display reply
	(goto-char previous-point)))))

;; Unused? -fp
;(defun twelf-backwards-parse-arglist ()
;  "Parse an argument list template as returned by the server."
;  (save-window-excursion
;    (let ((twelf-server-buffer (twelf-get-server-buffer)))
;      (set-buffer twelf-server-buffer)
;      (goto-char *twelf-server-last-process-mark*)
;      ;; Should be right at the beginning of the output.
;      ;; (re-search-forward "^arglist") ;
;      ;; (beginning-of-line 2)
;      (let ((arglist-begin (point)))
;        (skip-chars-forward "^." (point-max))
;        (buffer-substring arglist-begin (point))))))

;; Not yet ported to Twelf 1.2
;(defun twelf-show-region-in-window (start end)
;  "Change window parameters so it precisely shows the given region."
;  (enlarge-window (- (max (count-lines start end) window-min-height)
;                     (window-height)))
;  (set-window-start (selected-window) start))

;(defun twelf-show-menu ()
;  "Display the Twelf server buffer to show menu of possible completions."
;  (let ((old-buffer (current-buffer))
;        (twelf-server-buffer (twelf-get-server-buffer))
;        region-start region-end)
;    (switch-to-buffer-other-window twelf-server-buffer)
;    (goto-char *twelf-server-last-process-mark*)
;    (if (re-search-forward "-\\.$" (point-max) t)
;        (progn
;          (forward-char 1)
;          (setq region-start (point))
;          (if (re-search-forward "^-\\." (point-max) t)
;              (setq region-end (point))
;            (error "List of alternatives not terminated by -.")))
;      (error "No alternatives found."))
;    (twelf-show-region-in-window region-start region-end)
;    (switch-to-buffer-other-window old-buffer)))

;(defun twelf-completions-at-point ()
;  "List the possible completions of the term at point based on type information.

;The possible completions are numbered, and the function twelf-complete
;(\\[twelf-complete]) can be used subsequently to replace the term at point with
;one of the alternatives.

;Above the display of the alternatives, the type of the subterm at
;point is shown, since it is this type which is the basis for listing
;the possible completions.

;In the list alternatives, a variable X free in the remaining declaration
;is printed ^X, and a bound variable x may be printed as !x.  These marks
;are intended to aid in the understanding of the alternatives, but
;must be removed in case the alternative is copied literally into the
;input declaration (as, for example, with the \\[twelf-complete] command)."
;  (interactive)
;  (let* ((par (twelf-current-decl))
;         (par-start (nth 0 par))
;         (par-end (nth 1 par))
;         (decl (twelf-buffer-substring-dot par-start par-end)))
;    (twelf-focus par-start par-end)
;    (twelf-server-send-command
;     (concat "complete-at "
;             (twelf-current-syncat) " "
;             (int-to-string (+ (- (point) par-start) 2)) "\n"
;             decl))
;    (twelf-server-wait nil)
;    (twelf-highlight-range par-start par-end)
;    (twelf-show-menu)))

;(defun twelf-complete (n)
;  "Pick the alternative N from among possible completions.
;This replaces the current region with the given pattern.
;The list of completions must be generated with the command
;twelf-completions-at-point (\\[twelf-completions-at-point])."
;  (interactive "NAlternative: ")
;  (let (start completion)
;    (save-excursion
;      (set-buffer (twelf-get-server-buffer))
;      (goto-char *twelf-server-last-process-mark*)
;      (if (not (re-search-forward (concat "^" (int-to-string n) "\\. ")
;                                  (point-max) t))
;          (error "No alternative %d found in Twelf server buffer." n))
;      (setq start (point))
;      (if (not (search-forward " ::" (point-max) t))
;          (error "List of completions not well-formed."))
;      (backward-char 3)
;      (setq completion (buffer-substring start (point))))
;    (delete-region (point) (mark))
;    (insert "(" completion ")")
;    (twelf-show-menu)))

;;;----------------------------------------------------------------------
;;; Twelf server mode (major mode)
;;; This is for the buffer with the Twelf server process, to facilitate
;;; direct interaction (which should rarely be necessary)
;;;----------------------------------------------------------------------

(defvar twelf-server-mode-map nil
  "The keymap used in twelf-server mode.")

(cond ((not twelf-server-mode-map)
       (setq twelf-server-mode-map (copy-keymap comint-mode-map))
       (install-basic-twelf-keybindings twelf-server-mode-map)
       ;; C-c C-c is bound to twelf-save-check config in Twelf mode
       (define-key twelf-server-mode-map "\C-c\C-c" 'twelf-save-check-config)
       ;; Bind the function shadowed by the previous definition to C-c C-i
       (define-key twelf-server-mode-map "\C-c\C-i" 'comint-interrupt-subjob)
       ))

(defconst twelf-server-cd-regexp "^\\s *OS\\.chDir\\s *\\(.*\\)"
  "Regular expression used to match cd commands in Twelf server buffer.")

(defun looked-at-string (string n)
  "Substring of STRING consisting of Nth match."
  (substring string (match-beginning n) (match-end n)))

(defun twelf-server-directory-tracker (input)
  "Checks input for cd commands and changes default directory in buffer.
As a side effect, it resets *twelf-error-pos* and *twelf-last-region-sent*
to indicate interactive input.  Used as comint-input-filter-function in Twelf
server buffer."
  (if (twelf-input-filter input)
      (setq *twelf-last-region-sent* nil))
  (setq *twelf-last-input-buffer* (current-buffer))
  (setq *twelf-error-pos* (marker-position (process-mark (twelf-server-process))))
  (cond ((string-match twelf-server-cd-regexp input)
	 (let ((expanded-dir (expand-dir (looked-at-string input 1))))
	   (setq default-directory expanded-dir)
	   (pwd)))
	((string-match "^set\\s +chatter\\s +\\([0-9]\\)+" input)
	 (setq twelf-chatter (string-to-number (looked-at-string input 1))))
	;;((string-match "^set\\s +trace\\s +\\([0-9]\\)+" input)
	;; (setq twelf-trace (string-to-number (looked-at-string input 1))))
	((string-match "^set\\s-+\\(\\S-+\\)\\s-+\\(\\w+\\)" input)
	 (if (assoc (looked-at-string input 1) *twelf-track-parms*)
	     (set (cdr (assoc (looked-at-string input 1) *twelf-track-parms*))
		  (looked-at-string input 2))))))

(defun twelf-input-filter (input)
  "Function to filter strings before they are saved in input history.
We filter out all whitespace and anything shorter than two characters."
  (and (not (string-match "\\`\\s *\\'" input))
       (> (length input) 1)))

(defun twelf-server-mode ()
  "Major mode for interacting with an inferior Twelf server process.
Runs twelf-server-mode-hook.

The following commands are available:
\\{twelf-server-mode-map}"
  (interactive)
  (kill-all-local-variables)
  ;; Initialize comint parameters
  (comint-mode)
  (setq comint-prompt-regexp "^") ;; no prompt
  (setq comint-input-filter 'twelf-input-filter)
  ;;changed for XEmacs 19.16
  ;;(setq comint-input-sentinel 'twelf-server-directory-tracker)
  (add-hook 'comint-input-filter-functions 'twelf-server-directory-tracker
	    nil t)
  (twelf-mode-variables)
  ;; For sequencing through error messages:
  (make-local-variable '*twelf-error-pos*)
  (setq *twelf-error-pos* (point-max))
  ;; Set mode and keymap
  (setq major-mode 'twelf-server-mode)
  (setq mode-name "Twelf Server")
  (setq mode-line-process '(": %s"))
  (use-local-map twelf-server-mode-map)
  (twelf-server-add-menu)		; add Twelf Server menu
  ;; Run user specified hooks, if any
  (run-hooks 'twelf-server-mode-hook))

;;;----------------------------------------------------------------------
;;; Functions to support use of the Twelf server
;;;----------------------------------------------------------------------

(defun twelf-parse-config ()
  "Starting at point, parse a configuration file."
  (let ((filelist nil))
    (skip-chars-forward *whitespace*)
    (while (not (eobp))                 ; end of buffer?
      (cond ((looking-at "%")           ; comment through end of line
	     (end-of-line))
	    (t (let ((begin-point (point))) ; parse filename starting at point
		 (skip-chars-forward (concat "^" *whitespace*))
		 (let* ((file-name (buffer-substring begin-point (point)))
			(absolute-file-name
			 (expand-file-name file-name default-directory)))
		   (if (file-readable-p absolute-file-name)
		       (setq filelist (cons absolute-file-name filelist))
		     (error "File %s not readable." file-name))))))
      (skip-chars-forward *whitespace*))
    filelist))

(defun twelf-server-read-config ()
  "Read the configuration and initialize *twelf-config-list*."
  (if (or (not (bufferp *twelf-config-buffer*))
	  (null (buffer-name *twelf-config-buffer*)))
      (error "No current configuration buffer"))
  (set-buffer *twelf-config-buffer*)
  (goto-char (point-min))
  (twelf-parse-config))

(defun twelf-server-sync-config ()
  "Synchronize the configuration file, buffer, and Twelf server."
  (if (or (not (bufferp *twelf-config-buffer*))
	  (null (buffer-name *twelf-config-buffer*)))
      (error "No current configuration buffer"))
  (if (and twelf-config-mode
	   (not (equal *twelf-config-buffer* (current-buffer)))
	   (yes-or-no-p "Buffer is different from current configuration, reconfigure server? "))
      (twelf-server-configure (buffer-file-name (current-buffer))
			      "Server OK: Reconfigured"))
  (save-excursion
    (set-buffer *twelf-config-buffer*)
    (if (buffer-modified-p *twelf-config-buffer*)
	(progn
	  (display-buffer *twelf-config-buffer*)
	  (if (yes-or-no-p "Config buffer has changed, save new version? ")
	      (save-buffer)
	    (message "Checking old configuration"))))
    (if (not (verify-visited-file-modtime *twelf-config-buffer*))
	(if (yes-or-no-p "Config file has changed, read new contents? ")
	    (revert-buffer t t)))
    (if (not (equal (visited-file-modtime) *twelf-config-time*))
	(progn
	  (display-buffer *twelf-config-buffer*)
	  (if (yes-or-no-p "Config file has changed, reconfigure server? ")
	      (twelf-server-configure (buffer-file-name *twelf-config-buffer*)
				    "Server OK: Configured")
	    (if (not (yes-or-no-p "Ask next time? "))
		(setq *twelf-config-time* (visited-file-modtime))))))))

(defun twelf-get-server-buffer (&optional createp)
  "Get the current Twelf server buffer.
Optional argument CREATEP indicates if the buffer should be
created if it doesn't exist."
  (if (and (bufferp *twelf-server-buffer*)
	   (not (null (buffer-name *twelf-server-buffer*))))
      *twelf-server-buffer*
    (if createp
	(let ((twelf-server-buffer
	       (get-buffer-create *twelf-server-buffer-name*)))
	  (save-window-excursion
	    (set-buffer twelf-server-buffer)
	    (twelf-server-mode)
	    (setq *twelf-server-buffer* twelf-server-buffer))
	  twelf-server-buffer)
      (error "No Twelf server buffer"))))

(defun twelf-init-variables ()
  "Initialize variables that track Twelf server state."
  (setq twelf-chatter 3)
  ;;(setq twelf-trace 0)
  (setq twelf-double-check "false")
  (setq twelf-print-implicit "false"))

(defun twelf-server (&optional program)
  "Start an Twelf server process in a buffer named *twelf-server*.
Any previously existing process is deleted after confirmation.
Optional argument PROGRAM defaults to the value of the variable
twelf-server-program.
This locally re-binds `twelf-server-timeout' to 15 secs."
  (interactive)
  (let* ((default-program (if (null program) twelf-server-program program))
	 (default-dir (file-name-directory default-program))
	 (program (expand-file-name
		   (if (null program)
		       (read-file-name (concat "Twelf server: (default "
					       (file-name-nondirectory
						default-program)
					       ") ")
				       default-dir
				       default-program
				       t)
		     program)))
	 ;; longer timeout during startup
	 (twelf-server-timeout 15))
    ;; We save the program name as the default for the next time a server is
    ;; started in this session.
    (setq twelf-server-program program))
  (save-window-excursion
    (let* ((twelf-server-buffer (twelf-get-server-buffer t))
	   (twelf-server-process (get-buffer-process twelf-server-buffer)))
      (set-buffer twelf-server-buffer)
      (if (not (null twelf-server-process))
	  (if (yes-or-no-p "Kill current server process? ")
	      (delete-process twelf-server-process)
	    (error "Twelf Server restart aborted")))
      (goto-char (point-max))
      (setq *twelf-server-last-process-mark* (point))
      ;; initialize variables
      (twelf-init-variables)
      (start-process *twelf-server-process-name*
		     twelf-server-buffer
		     twelf-server-program)
      (twelf-server-wait)
      (twelf-server-process))))

(defun twelf-server-process (&optional buffer)
  "Return the twelf server process, starting one if none exists."
  (let* ((twelf-server-buffer (if (null buffer) (twelf-get-server-buffer t)
			      buffer))
	 (twelf-server-process (get-buffer-process twelf-server-buffer)))
      (if (not (null twelf-server-process))
	  twelf-server-process
	  (twelf-server))))

(defun twelf-server-display (&optional selectp)
  "Display Twelf server buffer, moving to the end of output.
With prefix argument also selects the Twelf server buffer."
  (interactive "P")
  (display-server-buffer)
  (if selectp (pop-to-buffer (twelf-get-server-buffer))))

(defun display-server-buffer (&optional buffer)
  "Display the Twelf server buffer so that the end of output is visible."
  (let* ((twelf-server-buffer (if (null buffer) (twelf-get-server-buffer)
			      buffer))
	 (_ (set-buffer twelf-server-buffer))
	 (twelf-server-process (twelf-server-process twelf-server-buffer))
	 (proc-mark (process-mark twelf-server-process))
	 (_ (display-buffer twelf-server-buffer))
	 (twelf-server-window (get-buffer-window twelf-server-buffer)))
    (if (not (pos-visible-in-window-p proc-mark twelf-server-window))
	(progn
	  (push-mark proc-mark)
	  (set-window-point twelf-server-window proc-mark)))
    (sit-for 0)))

(defun twelf-server-send-command (command)
  "Send a string COMMAND to the Twelf server."
  (interactive "sCommand: ")
  (let* ((input (concat command "\n"))
	 (twelf-server-buffer (twelf-get-server-buffer))
	 (twelf-server-process (twelf-server-process twelf-server-buffer)))
    (if twelf-server-echo-commands
	(let ((previous-buffer (current-buffer)))
	  (if twelf-server-display-commands
	      (display-server-buffer twelf-server-buffer))
	  (set-buffer twelf-server-buffer)
	  (goto-char (point-max))
	  (insert input)
	  (set-marker (process-mark twelf-server-process) (point-max))
	  (setq *twelf-error-pos* (point-max))
	  (set-buffer previous-buffer)))
    (setq *twelf-last-input-buffer* twelf-server-buffer)
    (setq *twelf-server-last-process-mark*
	  (marker-position (process-mark twelf-server-process)))
    (comint-send-string twelf-server-process input)))

(defun twelf-accept-process-output (process timeout)
  "Incompatibility workaround for versions of accept-process-output.
In case the function accepts no TIMEOUT argument, we wait potentially
forever (until the user aborts, typically with \\[keyboard-quit])."
  (condition-case nil			; do not keep track of error message
      (accept-process-output process timeout)
    (wrong-number-of-arguments
     (accept-process-output process))))

(defun twelf-server-wait (&optional displayp ok-message abort-message)
  "Wait for server acknowledgment and beep if error occurred.
If optional argument DISPLAYP is non-NIL, or if an error occurred, the
Twelf server buffer is displayed.  Optional second and third arguments
OK-MESSAGE and ABORT-MESSAGE are the strings to show upon successful
completion or abort of the server which default to \"Server OK\" and
\"Server ABORT\"."
  (let* ((chunk-count 0)
	 (last-point *twelf-server-last-process-mark*)
	 (previous-buffer (current-buffer))
	 (previous-match-data (match-data))
	 (twelf-server-buffer (twelf-get-server-buffer))
	 (twelf-server-process (get-buffer-process twelf-server-buffer)))
    (unwind-protect
	(catch 'done
	  (set-buffer twelf-server-buffer)
	  (while t
	    (goto-char last-point)
	    (if (re-search-forward "\\(%% OK %%\n\\)\\|\\(%% ABORT %%\n\\)"
				   (point-max) 'limit)
		(cond ((match-beginning 1)
		       (if displayp
			   (display-server-buffer twelf-server-buffer))
		       (message (or ok-message "Server OK"))
		       (throw 'done nil))
		      ((match-beginning 2)
		       (display-server-buffer twelf-server-buffer)
		       (error (or abort-message "Server ABORT"))
		       (throw 'done nil)))
	      (cond ((or (not (twelf-accept-process-output
			       twelf-server-process twelf-server-timeout))
			 (= last-point (point)))
		     (display-server-buffer twelf-server-buffer)
		     (message "Server TIMEOUT, continuing Emacs")
		     (throw 'done nil))
		    (t (setq chunk-count (+ chunk-count 1))
		       (if (= (mod chunk-count 10) 0)
			   (message (make-string (/ chunk-count 10) ?#)))
		       (sit-for 0))))))
      (store-match-data previous-match-data)
      (set-buffer previous-buffer))))

(defun twelf-server-quit ()
  "Kill the Twelf server process."
  (interactive)
  (twelf-server-send-command "OS.exit"))

(defun twelf-server-interrupt ()
  "Interrupt the Twelf server process."
  (interactive)
  (interrupt-process (twelf-server-process)))

(defun twelf-reset ()
  "Reset the global signature of Twelf maintained by the server."
  (interactive)
  (twelf-server-send-command "reset"))

(defun twelf-config-directory ()
  "Returns directory with current Twelf server configuration."
  (let ((config-file (buffer-file-name *twelf-config-buffer*)))
    (file-name-directory config-file)))

;(defun relativize-file-name (filename dir)
;  "Relativize FILENAME with respect to DIR, if possible."
;  (if (string= dir (file-name-directory filename))
;      (file-name-nondirectory filename)
;    filename))

(defun twelf-server-configure (config-file &optional ok-message)
  "Initializes the Twelf server configuration from CONFIG-FILE.
A configuration file is a list of relative file names in
dependency order.  Lines starting with % are treated as comments.
Starts a Twelf servers if necessary."
  (interactive
   (list (if twelf-config-mode (buffer-file-name)
	   (expand-file-name
	    (read-file-name "Visit config file: (default sources.cfg) "
			    default-directory
			    (concat default-directory "sources.cfg")
			    nil ; don't require match for now
			    )))))
  (let* ((config-file (if (file-directory-p config-file)
			  (concat config-file "sources.cfg")
			config-file))
	 (config-file-os (twelf-convert-standard-filename config-file))
	 (config-dir (file-name-directory config-file))
	 (config-dir-os (twelf-convert-standard-filename config-dir))
	 (config-buffer (set-buffer (or (get-file-buffer config-file)
					(find-file-noselect config-file))))
	 config-list)
    (setq *twelf-config-buffer* config-buffer)
    (if (and (not (verify-visited-file-modtime (get-file-buffer config-file)))
	     (yes-or-no-p "Config file has changed, read new contents? "))
	(revert-buffer t t))
    (setq config-list (twelf-server-read-config))
    (twelf-server-process)                ; Start process if necessary
    (let* ((_ (set-buffer (twelf-get-server-buffer)))
	   (cd-command
	    (if (equal default-directory config-dir)
		nil
	      (setq default-directory config-dir)
	      (concat "OS.chDir " config-dir-os)))
	   (_ (set-buffer config-buffer)))
      (cond ((not (null cd-command))
	     (twelf-server-send-command cd-command)
	     (twelf-server-wait nil ""
				"Server ABORT: Could not change directory")))
      (twelf-server-send-command
       (concat "Config.read " config-file-os))
      (twelf-server-wait nil (or ok-message "Server OK")
		       "Server ABORT: Could not be configured")
      ;; *twelf-config-buffer* should still be current buffer here
      (setq *twelf-config-time* (visited-file-modtime))
      (setq *twelf-config-list* config-list))))

;(defun twelf-server-add-file (filename)
;  "Adds a file to the current configuration."
;  (interactive
;   (list (expand-file-name
;          (read-file-name "File to add: " (twelf-config-directory)))))
;  (let ((relative-file (file-relative-name filename (twelf-config-directory)))
;	temp-time)
;    (save-excursion
;      (set-buffer *twelf-config-buffer*)
;      (goto-char (point-max))
;      (if (not (= (point) (point-min)))
;          (progn
;            (backward-char 1)
;            (if (looking-at "\n")
;                (forward-char 1)
;              (forward-char 1)
;              (insert "\n"))))
;      (insert (concat relative-file "\n"))
;      (save-buffer)
;      (setq temp-time (visited-file-modtime)))
;    (twelf-server-send-command
;     (concat "Config.read " (buffer-file-name *twelf-config-buffer*)))
;    (twelf-server-wait nil "" "Server ABORT: File could not be added to configuration")
;    (setq *twelf-config-list* (cons filename *twelf-config-list*))
;    (setq *twelf-config-time* temp-time)))

(defun natp (x)
  "Checks if X is an integer greater or equal to 0."
  (and (integerp x) (>= x 0)))

(defun twelf-read-nat ()
  "Reads a natural number from the minibuffer."
  (let ((num nil))
    (while (not (natp num))
      (setq num (read-from-minibuffer "Number: " (if num (prin1-to-string num))
				      nil t t))
      (if (not (natp num)) (beep)))
    num))

(defun twelf-read-bool ()
  "Read a boolean in mini-buffer."
  (completing-read "Boolean: "
		   '(("true" . true) ("false" . false))
		   nil t))

(defun twelf-read-limit ()
  "Read a limit (* or natural number) in mini-buffer."
  (let ((input (read-string "Limit (* or nat): ")))
    (if (equal input "*")
	input
      (let ((n (string-to-number input)))
	(if (and (integerp n) (> n 0))
	    n
	  (error "Number must be non-negative integer"))))))

(defun twelf-read-strategy ()
  "Read a strategy in mini-buffer."
  (completing-read "Strategy: "
		   '(("FRS" . "FRS") ("RFS" . "RFS"))
		   nil t))

(defun twelf-read-value (argtype)
  "Call the read function appropriate for ARGTYPE and return result."
  (funcall (cdr (assoc argtype *twelf-read-functions*))))

(defun twelf-set (parm value)
  "Sets the Twelf parameter PARM to VALUE.
When called interactively, prompts for parameter and value, supporting
completion."
  (interactive
   (let* ((parm (completing-read
		 "Parameter: " *twelf-parm-table* nil t))
	  (argtype (cdr (assoc parm *twelf-parm-table*)))
	  (value (twelf-read-value argtype)))
     (list parm value)))
  (track-parm parm value)		; track, if necessary
  (twelf-server-send-command (concat "set " parm " " value)))

(defun twelf-set-parm (parm)
  "Prompts for and set the value of Twelf parameter PARM.
Used in menus."
  (let* ((argtype (cdr (assoc parm *twelf-parm-table*)))
	 (value (and argtype (twelf-read-value argtype))))
    (if (null argtype)
	(error "Unknown parameter")
      (twelf-set parm value))))

(defun track-parm (parm value)
  "Tracks Twelf parameter values in Emacs."
  (if (assoc parm *twelf-track-parms*)
      (set (cdr (assoc parm *twelf-track-parms*)) value)))

(defun twelf-toggle-double-check ()
  "Toggles doubleCheck parameter of Twelf."
  (let ((value (if (string-equal twelf-double-check "false")
		   "true" "false")))
    (twelf-set "doubleCheck" value)))

(defun twelf-toggle-print-implicit ()
  "Toggles Print.implicit parameter of Twelf."
  (let ((value (if (string-equal twelf-print-implicit "false")
		   "true" "false")))
    (twelf-set "Print.implicit" value)))

(defun twelf-get (parm)
  "Prints the value of the Twelf parameter PARM.
When called interactively, promts for parameter, supporting completion."
  (interactive (list (completing-read "Parameter: " *twelf-parm-table* nil t)))
  (twelf-server-send-command (concat "get " parm))
  (twelf-server-wait)
  (save-window-excursion
    (let ((twelf-server-buffer (twelf-get-server-buffer)))
      (set-buffer twelf-server-buffer)
      (goto-char *twelf-server-last-process-mark*)
      ;; We are now at the beginning of the output
      (end-of-line 1)
      (message (buffer-substring *twelf-server-last-process-mark* (point))))))

(defun twelf-timers-reset ()
  "Reset the Twelf timers."
  (interactive)
  (twelf-server-send-command "Timers.reset"))

(defun twelf-timers-show ()
  "Show and reset the Twelf timers."
  (interactive)
  (twelf-server-send-command "Timers.show")
  (twelf-server-wait t))

(defun twelf-timers-check ()
  "Show the Twelf timers without resetting them."
  (interactive)
  (twelf-server-send-command "Timers.show")
  (twelf-server-wait t))

(defun twelf-server-restart ()
  "Restarts server and re-initializes configuration.
This is primarily useful during debugging of the Twelf server code or
if the Twelf server is hopelessly wedged."
  (interactive)
  (twelf-server twelf-server-program)
  (twelf-server-configure (if *twelf-config-buffer*
			    (buffer-file-name *twelf-config-buffer*)
			  "sources.cfg")
			"Server configured, now checking...")
  (twelf-check-config))

;;;----------------------------------------------------------------------
;;; Twelf Config minor mode
;;;----------------------------------------------------------------------

(defun twelf-config-mode (&optional prefix)
  "Toggles minor mode for Twelf configuration files.
This affects \\<twelf-mode-map>
 twelf-server-configure (\\[twelf-server-configure])
 twelf-save-check-config (\\[twelf-save-check-config])
"
  (interactive "P")
  (make-local-variable 'twelf-config-mode)
  (cond ((not (assq 'twelf-config-mode minor-mode-alist))
	 (setq minor-mode-alist
	       (cons '(twelf-config-mode " Config") minor-mode-alist))))
  (cond ((or (not twelf-config-mode) prefix)
	 (setq twelf-config-mode t)
	 (run-hooks 'twelf-config-mode-hook))
	(t (setq twelf-config-mode t))))

(defun twelf-config-mode-check (&optional buffer)
  "Switch on the Twelf Config minor mode if the ends in `.cfg'."
  (if (string-match "\\.cfg$" (buffer-file-name (or buffer (current-buffer))))
      (twelf-config-mode t)))

;;;----------------------------------------------------------------------
;;; Support for creating a TAGS file for current Twelf server configuration
;;;----------------------------------------------------------------------

(defun twelf-tag (&optional tags-filename)
  "Create tags file for current configuration.
If the current configuration is sources.cfg, the tags file is TAGS.
If current configuration is named FILE.cfg, tags file will be named FILE.tag
Errors are displayed in the Twelf server buffer.
Optional argument TAGS-FILENAME specifies alternative filename."
  (interactive)
  (twelf-server-sync-config)
  (let* ((error-buffer (twelf-get-server-buffer))
	 (config-filename (buffer-file-name *twelf-config-buffer*))
	 (tags-file
	  (or tags-filename
	      (if (string-equal "sources.cfg"
				(file-name-nondirectory config-filename))
		  (concat (file-name-directory config-filename "TAGS"))
		(concat (file-name-sans-extension config-filename)
			".tag")))))
    (save-excursion
      (set-buffer error-buffer)
      (goto-char (point-max))
      (insert "Tagging configuration " config-filename " in file " tags-file "\n"))
    (set-buffer *twelf-config-buffer*)
    (twelf-tag-files (rev-relativize *twelf-config-list* default-directory)
		   tags-file error-buffer)
    (if (get-buffer-process error-buffer)
	(set-marker (process-mark (get-buffer-process error-buffer))
		    (point-max)))))

(defun twelf-tag-files (filelist &optional tags-filename error-buffer)
  "Create tags file for FILELIST, routing errors to buffer *tags-errors*.
Optional argument TAGS-FILENAME specifies alternative filename (default: TAGS),
optional argument ERROR-BUFFER specifies alternative buffer for error message
(default: *tags-errors*)."
  (let* ((tags-filename (or tags-filename "TAGS"))
	 (tags-buffer (find-file-noselect tags-filename))
	 (error-buffer (or error-buffer (new-temp-buffer "*tags-errors*"))))
    (save-excursion
      (set-buffer tags-buffer)
      (if (equal (point-min) (point-max))
	  nil
	;;(pop-to-buffer tags-buffer)
	;;(if (yes-or-no-p "Delete current tags information? ")
	(delete-region (point-min) (point-max))
	;;)
	))
    (switch-to-buffer-other-window error-buffer)
    (while (not (null filelist))
      (twelf-tag-file (car filelist) tags-buffer error-buffer)
      (setq filelist (cdr filelist)))
    (save-excursion
      (set-buffer tags-buffer)
      (save-buffer))))

(defun twelf-tag-file (filename tags-buffer error-buffer)
  "Deposit tag information for FILENAME in TAGS-BUFFER, errors in ERROR-BUFFER."
  (let ((src-buffer (find-file-noselect filename))
	file-start file-end end-of-id tag-string)
    (save-excursion
      (set-buffer tags-buffer)
      (goto-char (point-max))
      (insert "\f\n" filename ",0\n")
      (setq file-start (point))
      (save-excursion
	(set-buffer src-buffer)
	(goto-char (point-min))
	(while (twelf-next-decl filename error-buffer)
	  (setq end-of-id (point))
	  (beginning-of-line 1)
	  (setq tag-string
		(concat (buffer-substring (point) end-of-id)
			"\C-?" (current-line-absolute) "," (point) "\n"))
	  (goto-char end-of-id)
	  (if (not (twelf-end-of-par))
	      (let ((error-line (current-line-absolute)))
		(save-excursion
		  (set-buffer error-buffer)
		  (goto-char (point-max))
		  (insert filename ":" (int-to-string error-line)
			  " Warning: missing period\n"))))
	  (save-excursion
	    (set-buffer tags-buffer)
	    (insert tag-string))))
      (setq file-end (point-max))
      (goto-char (- file-start 2))
      (delete-char 1)
      (insert (int-to-string (- file-end file-start)))
      (goto-char (point-max)))))

(defun twelf-next-decl (filename error-buffer)
  "Set point after the identifier of the next declaration.
Return the declared identifier or `nil' if none was found.
FILENAME and ERROR-BUFFER are used if something appears wrong."
  (let ((id nil)
	end-of-id
	beg-of-id)
    (skip-twelf-comments-and-whitespace)
    (while (and (not id) (not (eobp)))
      (setq beg-of-id (point))
      (if (zerop (skip-chars-forward *twelf-id-chars*))
	  ;; Not looking at id: skip ahead
	  (skip-ahead filename (current-line-absolute) "No identifier"
		      error-buffer)
	(setq end-of-id (point))
	(skip-twelf-comments-and-whitespace)
	(if (not (looking-at ":"))
	    ;; Not looking at valid decl: skip ahead
	    (skip-ahead filename (current-line-absolute end-of-id) "No colon"
			error-buffer)
	  (goto-char end-of-id)
	  (setq id (buffer-substring beg-of-id end-of-id))))
      (skip-twelf-comments-and-whitespace))
    id))

(defun skip-ahead (filename line message error-buffer)
  "Skip ahead when syntactic error was found.
A parsable error message constited from FILENAME, LINE, and MESSAGE is
deposited in ERROR-BUFFER."
  (if error-buffer
      (save-excursion
	(set-buffer error-buffer)
	(goto-char (point-max))
	(insert filename ":" (int-to-string line) " Warning: " message "\n")
	(setq *twelf-error-pos* (point))))
  (twelf-end-of-par))

(defun current-line-absolute (&optional char-pos)
  "Return line number of CHAR-POS (default: point) in current buffer.
Ignores any possible buffer restrictions."
  (1+ (count-lines 1 (or char-pos (point)))))

(defun new-temp-buffer (&optional name)
  "Create or delete contents of buffer named \"*temp*\" and return it.
Optional argument NAME specified an alternative name."
  (if (not name) (setq name "*temp*"))
  (if (get-buffer name)
      (save-excursion
	(set-buffer name)
	(delete-region (point-min) (point-max))
	(get-buffer name))
    (get-buffer-create name)))

(defun rev-relativize (filelist dir)
  "Reverse and relativize FILELIST with respect to DIR."
  (let ((newlist nil))
    (while (not (null filelist))
      (setq newlist
	    (cons (file-relative-name (car filelist) dir) newlist))
      (setq filelist (cdr filelist)))
    newlist))


;;;----------------------------------------------------------------------
;;; Twelf-SML mode
;;;----------------------------------------------------------------------

(defvar twelf-sml-mode-map nil
  "The keymap used in Twelf-SML mode.")

(cond ((not twelf-sml-mode-map)
       ;;(setq twelf-sml-mode-map (full-copy-sparse-keymap comint-mode-map))
       ;; fixed for Emacs 19.25.  -fp Thu Oct 27 09:08:44 1994
       (setq twelf-sml-mode-map (copy-keymap comint-mode-map))
       (install-basic-twelf-keybindings twelf-sml-mode-map)
       ))

(defconst twelf-sml-prompt-regexp "^\\- \\|^\\?\\- ")

(defun expand-dir (dir)
  "Expand argument and check that it is a directory."
  (let ((expanded-dir (file-name-as-directory (expand-file-name dir))))
    (if (not (file-directory-p expanded-dir))
	(error "%s is not a directory" dir))
    expanded-dir))

(defun twelf-sml-cd (dir)
  "Make DIR become the Twelf-SML process' buffer's default directory and
furthermore issue an appropriate command to the inferior Twelf-SML process."
  (interactive "DChange default directory: ")
  (let ((expanded-dir (expand-dir dir)))
    (save-excursion
      (set-buffer (twelf-sml-process-buffer))
      (setq default-directory expanded-dir)
      (comint-simple-send (twelf-sml-process) (concat "Twelf.OS.chDir \"" expanded-dir "\";")))
    ;;(pwd)
    ))

(defconst twelf-sml-cd-regexp "^\\s *cd\\s *\"\\([^\"]*\\)\""
  "Regular expression used to match cd commands in Twelf-SML buffer.")

(defun twelf-sml-directory-tracker (input)
  "Checks input for cd commands and changes default directory in buffer.
As a side-effect, it sets *twelf-last-region-sent* to NIL to indicate interactive
input.  As a second side-effect, it resets the *twelf-error-pos*.
Used as comint-input-sentinel in Twelf-SML buffer."
  (if (twelf-input-filter input)
      (setq *twelf-last-region-sent* nil))
  (setq *twelf-last-input-buffer* (current-buffer))
  (setq *twelf-error-pos* (marker-position (process-mark (twelf-sml-process))))
  (cond ((string-match twelf-sml-cd-regexp input)
	 (let ((expanded-dir (expand-dir (substring input
						    (match-beginning 1)
						    (match-end 1)))))
	   (setq default-directory expanded-dir)
	   (pwd)))))

(defun twelf-sml-mode ()
  "Major mode for interacting with an inferior Twelf-SML process.

The following commands are available:
\\{twelf-sml-mode-map}

An Twelf-SML process can be started with \\[twelf-sml].

Customisation: Entry to this mode runs the hooks on twelf-sml-mode-hook.

You can send queries to the inferior Twelf-SML process from other buffers.

Commands:
Return after the end of the process' output sends the text from the
    end of process to point.
Return before the end of the process' output copies the current line
    to the end of the process' output, and sends it.
Delete converts tabs to spaces as it moves back.
Tab indents for Twelf; with argument, shifts rest
    of expression rigidly with the current line.
C-M-q does Tab on each line starting within following expression.
Paragraphs are separated only by blank lines.  % start single comments,
delimited comments are enclosed in %{...}%.
If you accidentally suspend your process, use \\[comint-continue-subjob]
to continue it."
  (interactive)
  (kill-all-local-variables)
  (comint-mode)
  (setq comint-prompt-regexp twelf-sml-prompt-regexp)
  (setq comint-input-filter 'twelf-input-filter)
  ;; changed for XEmacs 19.16 Sat Jun 13 11:28:53 1998
  (add-hook 'comint-input-filter-functions 'twelf-sml-directory-tracker
	    nil t)
  (twelf-mode-variables)

  ;; For sequencing through error messages:
  (make-local-variable '*twelf-error-pos*)
  (setq *twelf-error-pos* (point-max))
  ;; Workaround for problem with Lucid Emacs version of comint.el:
  ;; must exclude double quotes " and must include $ and # in filenames.
  (make-local-variable 'comint-match-partial-pathname-chars)
  (setq comint-match-partial-pathname-chars
	"^][<>{}()!^&*\\|?`'\" \t\n\r\b")

  (setq major-mode 'twelf-sml-mode)
  (setq mode-name "Twelf-SML")
  (setq mode-line-process '(": %s"))
  (use-local-map twelf-sml-mode-map)

  (run-hooks 'twelf-sml-mode-hook))

(defun twelf-sml (&optional cmd)
  "Run an inferior Twelf-SML process in a buffer *twelf-sml*.
If there is a process already running in *twelf-sml*, just
switch to that buffer.  With argument, allows you to change the program
which defaults to the value of twelf-sml-program.  Runs the hooks from
twelf-sml-mode-hook (after the comint-mode-hook is run).

Type \\[describe-mode] in the process buffer for a list of commands."
  (interactive (list (and current-prefix-arg
			  (read-string "Run Twelf-SML: " twelf-sml-program))))
  (let ((cmd (or cmd twelf-sml-program)))
    (cond ((not (comint-check-proc (twelf-sml-process-buffer)))
	   ;; process does not already exist
	   (set-buffer (apply 'make-comint "twelf-sml" cmd nil twelf-sml-args))
	   ;; in case we are using SML mode (for error tracking)
	   (if (boundp 'sml-buffer)
	       (set 'sml-buffer (twelf-sml-process-buffer)))
	   (twelf-sml-mode))))
  (switch-to-buffer (twelf-sml-process-buffer)))

(defun switch-to-twelf-sml (eob-p)
  "Switch to the Twelf-SML process buffer.
With argument, positions cursor at end of buffer."
  (interactive "P")
  (if (twelf-sml-process-buffer)
      (pop-to-buffer (twelf-sml-process-buffer))
      (error "No current process buffer. "))
  (cond (eob-p
	 (push-mark)
	 (goto-char (point-max)))))

(defun display-twelf-sml-buffer (&optional buffer)
  "Display the Twelf-SML buffer so that the end of output is visible."
  ;; Accept output from Twelf-SML process
  (sit-for 1)
  (let* ((twelf-sml-buffer (if (null buffer) (twelf-sml-process-buffer)
		       buffer))
	 (_ (set-buffer twelf-sml-buffer))
	 (twelf-sml-process (twelf-sml-process))
	 (proc-mark (process-mark twelf-sml-process))
	 (_ (display-buffer twelf-sml-buffer))
	 (twelf-sml-window (get-buffer-window twelf-sml-buffer)))
    (if (not (pos-visible-in-window-p proc-mark twelf-sml-window))
	(progn
	  (push-mark proc-mark)
	  (set-window-point twelf-sml-window proc-mark)))))

(defun twelf-sml-send-string (string)
  "Send the given string to the Twelf-SML process."
  (setq *twelf-last-input-buffer* (twelf-sml-process-buffer))
  (comint-send-string (twelf-sml-process) string))

(defun twelf-sml-send-region (start end &optional and-go)
  "Send the current region to the inferior Twelf-SML process.
Prefix argument means switch-to-twelf-sml afterwards.
If the region is short, it is sent directly, via COMINT-SEND-REGION."
  (interactive "r\nP")
  (if (> start end)
      (twelf-sml-send-region end start and-go)
    ;; (setq twelf-sml-last-region-sent (list (current-buffer) start end))
    (let ((cur-buffer (current-buffer))
	  (twelf-sml-buffer (twelf-sml-process-buffer)))
      (switch-to-buffer twelf-sml-buffer)
      ;; (setq sml-error-pos (marker-position (process-mark (twelf-sml-process))))
      (setq *twelf-last-input-buffer* twelf-sml-buffer)
      (switch-to-buffer cur-buffer))
    (comint-send-region (twelf-sml-process) start end)
    (if (not (string= (buffer-substring (1- end) end) "\n"))
	(comint-send-string (twelf-sml-process) "\n"))
    ;; Next two lines mess up when an Twelf error occurs, since the
    ;; newline is not read and later messes up counting.
    ;; (if (not and-go)
    ;;  (comint-send-string (twelf-sml-process) "\n"))
    (if and-go (switch-to-twelf-sml t)
      (if twelf-sml-display-queries (display-twelf-sml-buffer)))))

(defun twelf-sml-send-query (&optional and-go)
  "Send the current declaration to the inferior Twelf-SML process as a query.
Prefix argument means switch-to-twelf-sml afterwards."
  (interactive "P")
  (let* ((par (twelf-current-decl))
	 (query-start (nth 0 par))
	 (query-end (nth 1 par)))
    (twelf-sml-set-mode 'TWELF)
    (twelf-sml-send-region query-start query-end and-go)))

(defun twelf-sml-send-newline (&optional and-go)
  "Send a newline to the inferior Twelf-SML process.
If a prefix argument is given, switches to Twelf-SML buffer afterwards."
  (interactive "P")
  (twelf-sml-send-string "\n")
  (if and-go (switch-to-twelf-sml t)
    (if twelf-sml-display-queries (display-twelf-sml-buffer))))

(defun twelf-sml-send-semicolon (&optional and-go)
  "Send a semi-colon to the inferior Twelf-SML process.
If a prefix argument is given, switched to Twelf-SML buffer afterwards."
  (interactive "P")
  (twelf-sml-send-string ";\n")
  (if and-go (switch-to-twelf-sml t)
    (if twelf-sml-display-queries (display-twelf-sml-buffer))))

(defun twelf-sml-status (&optional buffer)
  "Returns the status of the Twelf-SML process.
This employs a heuristic, looking at the contents of the Twelf-SML buffer.
Results:
 NONE --- no process
 ML   --- ML top level
 TWELF  --- Twelf top level
 MORE --- asking whether to find the next solution
 UNKNOWN --- process is running, but can't tell status."
  (let* ((twelf-sml-buffer (or buffer (twelf-sml-process-buffer)))
	 (twelf-sml-process (get-buffer-process twelf-sml-buffer)))
    (if (null twelf-sml-process)
	'NONE
      (save-excursion
	(set-buffer twelf-sml-buffer)
	(let ((buffer-end (buffer-substring (max (point-min) (- (point-max) 3))
					    (point-max))))
	  (cond ((string-match "\\?- " buffer-end) 'TWELF)
		((string-match "\n- " buffer-end) 'ML)
		((string-match "More\\? " buffer-end) 'MORE)
		(t 'UNKNOWN)))))))

(defvar twelf-sml-init "Twelf.Config.load (Twelf.Config.read \"sources.cfg\");\n"
  "Initial command sent to Twelf-SML process when started during twelf-sml-set-mode 'TWELF.")

(defun twelf-sml-set-mode (mode &optional buffer)
  "Attempts to read and if necessary correct the mode of the Twelf-SML buffer.
This does not check if the status has been achieved.  It returns NIL
if the status is unknown and T if it believes the status should have
been achieved.  This allows for asynchronous operation."
  (cond
    ((eq mode 'ML)
     (let ((status (twelf-sml-status)))
       (cond ((eq status 'NONE) (twelf-sml) 't)
	     ((eq status 'ML) 't)
	     ((eq status 'TWELF) (twelf-sml-send-string "") 't)
	     ((eq status 'MORE) (twelf-sml-send-string "q\n") 't)
	     ((eq status 'UNKNOWN) nil))))
    ((eq mode 'TWELF)
     (let ((status (twelf-sml-status)))
       (cond ((eq status 'NONE)
	      (twelf-sml)
	      (twelf-sml-send-string twelf-sml-init)
	      (twelf-sml-send-string "Twelf.top ();\n") 't)
	     ((eq status 'ML)
	      (twelf-sml-send-string "Twelf.top ();\n") 't)
	     ((eq status 'TWELF) 't)
	     ((eq status 'MORE) (twelf-sml-send-string "\n") 't)
	     ((eq status 'UNKNOWN) nil))))
    (t (error "twelf-sml-set-mode: illegal mode %s" mode))))

(defun twelf-sml-quit ()
  "Kill the Twelf-SML process."
  (interactive)
  (kill-process (twelf-sml-process)))

(defun twelf-sml-process-buffer ()
  "Returns the current Twelf-SML process buffer."
  (get-buffer "*twelf-sml*"))

(defun twelf-sml-process (&optional buffer)
  "Returns the current Twelf-SML process."
  (let ((proc (get-buffer-process (or buffer (twelf-sml-process-buffer)))))
    (or proc
	(error "No current process."))))

;;;----------------------------------------------------------------------
;;; 2Twelf-SML minor mode for Twelf
;;; Some keybindings now refer to Twelf-SML instead of the Twelf server.
;;; Toggle with twelf-to-twelf-sml-mode
;;;----------------------------------------------------------------------

(defvar twelf-to-twelf-sml-mode nil
  "Non-NIL means the minor mode is in effect.")

(defun install-twelf-to-twelf-sml-keybindings (map)
  ;; Process commands:
  (define-key map "\C-c\C-r" 'twelf-sml-send-region)
  (define-key map "\C-c\C-e" 'twelf-sml-send-query)
  (define-key map "\C-c\C-m" 'twelf-sml-send-newline)
  (define-key map "\C-c\n" 'twelf-sml-send-newline)
  (define-key map "\C-c;" 'twelf-sml-send-semicolon)
  (define-key map "\C-cd" 'twelf-sml-cd)
  )

(defvar twelf-to-twelf-sml-mode-map nil
  "Keymap for twelf-to-twelf-sml minor mode.")

(cond ((not twelf-to-twelf-sml-mode-map)
       (setq twelf-to-twelf-sml-mode-map (make-sparse-keymap))
       (install-basic-twelf-keybindings twelf-to-twelf-sml-mode-map)
       (install-twelf-keybindings twelf-to-twelf-sml-mode-map)
       ;; The next line shadows certain bindings to refer to
       ;; Twelf-SML instead of the Twelf server.
       (install-twelf-to-twelf-sml-keybindings twelf-to-twelf-sml-mode-map)))

(defun twelf-to-twelf-sml-mode (&optional prefix)
  "Toggles minor mode for sending queries to Twelf-SML instead of Twelf server.
Specifically:   \\<twelf-to-twelf-sml-mode-map>
 \\[twelf-sml-send-query] (for sending queries),
 \\[twelf-sml-send-newline] (for sending newlines) and
 \\[twelf-sml-send-semicolon] (for sending `;')
are rebound.

Mode map
========
\\{twelf-to-twelf-sml-mode-map}
"
  (interactive "P")
  (make-local-variable 'twelf-to-twelf-sml-mode)
  (cond ((not (assq 'twelf-to-twelf-sml-mode minor-mode-alist))
	 (setq minor-mode-alist
	       (cons '(twelf-to-twelf-sml-mode " 2Twelf-SML")
		     minor-mode-alist))))
  (cond ((or (not twelf-to-twelf-sml-mode) prefix)
	 (setq twelf-to-twelf-sml-mode t)
	 (use-local-map twelf-to-twelf-sml-mode-map)
	 (run-hooks 'twelf-to-twelf-sml-mode-hook))
	(t
	 (setq twelf-to-twelf-sml-mode nil)
	 (use-local-map twelf-mode-map))))

;;;----------------------------------------------------------------------
;;; Twelf mode menus
;;; requires auc-menu utilities
;;;----------------------------------------------------------------------

(cond
 ((string-match "XEmacs" emacs-version) ;; XEmacs nee Lucid Emacs
  (defun radio (label callback condition)
    (vector label callback ':style 'radio ':selected condition))
  (defun toggle (label callback condition)
    (vector label callback ':style 'toggle ':selected condition))
  (defun disable-form (label callback condition)
    (vector label callback condition))
  )
 (t ;; FSF Emacs 19
  (defun radio (label callback condition)
    (vector label callback t))
  (defun toggle (label callback condition)
    (vector label callback t))
  (defun disable-form (label callback condition)
    (cond ((symbolp condition) (vector label callback condition))
	  (t (vector label callback t))))
  ))

(defconst twelf-at-point-menu
  '("At Point"
    ["Constant" twelf-type-const t]
    ;["Type" twelf-type-at-point nil]	;disabled for Twelf 1.2
    ;["Expected Type" twelf-expected-type-at-point nil] ;disabled
    ;["List Completions" twelf-completions-at-point nil]	;disabled
    ;["Complete" twelf-complete nil] ;disabled
    )
  "Menu for commands applying at point.")

(defconst twelf-server-state-menu
  '("Server State"
    ["Configure" twelf-server-configure t]
    ["Interrupt" twelf-server-interrupt t]
    ["Reset" twelf-reset t]
    ["Start" twelf-server t]
    ["Restart" twelf-server-restart t]
    ["Quit" twelf-server-quit t])
  "Menu for commands affecting server state.")

(defconst twelf-error-menu
  '("Error Tracking"
    ["Next" twelf-next-error t]
    ["Goto" twelf-goto-error t])
  "Menu for error commands.")

(defconst twelf-tags-menu
  '("Tags"
    ["Find" find-tag t]
    ["Find Other Window" find-tag-other-window t]
    ["Query Replace" tags-query-replace t]
    ["Search" tags-search t]
    ["Continue" tags-loop-continue t]
    ["Create/Update" twelf-tag t])
  "Menu for tag commands.")

(defun twelf-toggle-server-display-commands ()
  (setq twelf-server-display-commands (not twelf-server-display-commands)))

(defconst twelf-options-menu
  `("Options"
    (, (toggle "Display Commands" '(twelf-toggle-server-display-commands)
	       'twelf-server-display-commands))
    ("chatter"
     (, (radio "0" '(twelf-set "chatter" 0) '(= twelf-chatter 0)))
     (, (radio "1" '(twelf-set "chatter" 1) '(= twelf-chatter 1)))
     (, (radio "2" '(twelf-set "chatter" 2) '(= twelf-chatter 2)))
     (, (radio "3*" '(twelf-set "chatter" 3) '(= twelf-chatter 3)))
     (, (radio "4" '(twelf-set "chatter" 4) '(= twelf-chatter 4)))
     (, (radio "5" '(twelf-set "chatter" 5) '(= twelf-chatter 5)))
     (, (radio "6" '(twelf-set "chatter" 6) '(= twelf-chatter 6))))
    (, (toggle "doubleCheck" '(twelf-toggle-double-check)
	       '(string-equal twelf-double-check "true")))
    ("Print."
     (, (toggle "implicit" '(twelf-toggle-print-implicit)
		'(string-equal twelf-print-implicit "true")))
     ["depth" (twelf-set-parm "Print.depth") t]
     ["length" (twelf-set-parm "Print.length") t]
     ["indent" (twelf-set-parm "Print.indent") t]
     ["width" (twelf-set-parm "Print.width") t])
    ("Prover."
     ["strategy" (twelf-set-parm "Prover.strategy") t]
     ["maxSplit" (twelf-set-parm "Prover.maxSplit") t]
     ["maxRecurse" (twelf-set-parm "Prover.maxRecurse") t])
    ;;["Trace" nil nil]
    ;; (, (radio "0" '(twelf-set "trace" 0) '(= twelf-trace 0)))
    ;; (, (radio "1" '(twelf-set "trace 1) '(= twelf-trace 1)))
    ;; (, (radio "2" '(twelf-set "trace" 2) '(= twelf-trace 2))))
    ;;["Untrace" nil nil]
    ;;(, (disable-form "Untrace" '(twelf-set "trace" 0)
    ;;	       '(not (= twelf-trace 0))))
    ["Reset Menubar" twelf-reset-menu t])
  "Menu to change options in Twelf mode.")

(defconst twelf-timers-menu
  '("Timing"
    ["Show and Reset" twelf-timers-show t]
    ["Check" twelf-timers-check t]
    ["Reset" twelf-timers-reset t]))

;(autoload 'toggle-twelf-font-immediate "twelf-font"
;  "Toggle experimental immediate highlighting in font-lock mode.")
(autoload 'twelf-font-fontify-decl "twelf-font"
  "Fontify current declaration using font-lock minor mode.")
(autoload 'twelf-font-fontify-buffer "twelf-font"
  "Fontify current buffer using font-lock minor mode.")

(defconst twelf-syntax-menu
  `("Syntax Highlighting"
    ["Highlight Declaration" twelf-font-fontify-decl t]
    ["Highlight Buffer" twelf-font-fontify-buffer t]
    ;;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate
    ;;'font-lock-mode))
    )
  "Menu for syntax highlighting in Twelf mode.")

(easy-menu-define twelf-menu (list twelf-mode-map)
  "Menu for Twelf mode.
This may be selected from the menubar.  In XEmacs, also bound to Button3."
  (list
   "Twelf"
   ["Display Server" twelf-server-display t]
   ["Check Configuration" twelf-save-check-config t]
   ["Check File" twelf-save-check-file t]
   ["Check Declaration" twelf-check-declaration t]
   twelf-at-point-menu
   twelf-error-menu
   twelf-options-menu
   twelf-syntax-menu
   twelf-tags-menu
   twelf-timers-menu
   twelf-server-state-menu
   ["Info" twelf-info t]))

(defun twelf-add-menu ()
  "Add Twelf menu to menubar."
  (easy-menu-add twelf-menu twelf-mode-map))

(defun twelf-remove-menu ()
  "Remove Twelf menu from menubar."
  (easy-menu-remove twelf-menu))

(defun twelf-reset-menu ()
  "Reset Twelf menu."
  (twelf-remove-menu)
  (twelf-add-menu))

;;;----------------------------------------------------------------------
;;; Twelf Server mode menu
;;;----------------------------------------------------------------------

(easy-menu-define twelf-server-menu (list twelf-server-mode-map)
  "Menu for Twelf Server mode.
This may be selected from the menubar.  In XEmacs, also bound to Button3."
  (list
   "Twelf-Server"
   ;; ["Display Server" twelf-server-display t]
   ["Check Configuration" twelf-save-check-config t]
   ;; ["Check File" twelf-save-check-file nil]
   ;; ["Check Declaration" twelf-check-declaration nil]
   ;; ["Check Query" twelf-check-query nil]
   ;; ["Solve Query" twelf-solve-query nil]
   ;; ["At Point" () nil]
   twelf-error-menu
   twelf-options-menu
   twelf-tags-menu
   twelf-server-state-menu
   ["Info" twelf-info t]))

(defun twelf-server-add-menu ()
  "Add Twelf menu to menubar."
  (easy-menu-add twelf-server-menu twelf-server-mode-map))

(defun twelf-server-remove-menu ()
  "Remove Twelf menu from menubar."
  (easy-menu-remove twelf-server-menu))

(defun twelf-server-reset-menu ()
  "Reset Twelf menu."
  (twelf-server-remove-menu)
  (twelf-server-add-menu))

(provide 'twelf-old)