diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-08-28 14:57:11 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-08-28 14:57:11 +0000 |
| commit | a85c79543c3203516226a414ccf3caff35c0c6e4 (patch) | |
| tree | a7d24ae09b29e69ca5227499f4ece01f019e6ed9 /twelf | |
| parent | 67f9fba4ee77d8ee23dd7f7f36676867e37d8243 (diff) | |
Files for twelf, not working at all yet.
Diffstat (limited to 'twelf')
| -rw-r--r-- | twelf/twelf-font.el | 318 | ||||
| -rw-r--r-- | twelf/twelf-old.el | 2661 | ||||
| -rw-r--r-- | twelf/twelf.el | 58 |
3 files changed, 3037 insertions, 0 deletions
diff --git a/twelf/twelf-font.el b/twelf/twelf-font.el new file mode 100644 index 00000000..0e7b8a13 --- /dev/null +++ b/twelf/twelf-font.el @@ -0,0 +1,318 @@ +;; twelf-font.el Font lock configuration for Twelf +;; +;; Author: Frank Pfenning +;; Taken from Twelf's emacs mode and +;; adapted for Proof General by David Aspinall <da@dcs.ed.ac.uk> +;; +;; $Id$ +;; +;; + +;; FIXME da: need to put syntax table into function + +;; modify the syntax table so _ and ' are word constituents +;; otherwise the regexp's for identifiers become very complicated +;; FIXME: fn undef'd(set-word ?\_) +;; FIXME: fn (set-word ?\') + +;; FIXME da: integrate with PG's face mechanism +;; (but maybe keep twelf faces to help users) + +;; setting faces here... +;; use devices to improve portability? +;; make it dependent on light background vs dark background +;; tie in X resources? + +(defun twelf-font-create-face (face from-face color) + "Creates a Twelf font from FROM-FACE with COLOR." + (make-face face) + ;(reset-face face) ; seems to be necessary, but why? + (copy-face from-face face) + (if color (set-face-foreground face color))) + +(defvar twelf-font-dark-background nil + "*T if the background of Emacs is to be considered dark.") + +;; currently we not using bold or italics---some font families +;; work poorly with that kind of face. +(cond (twelf-font-dark-background + (twelf-font-create-face 'twelf-font-keyword-face 'default nil) + (twelf-font-create-face 'twelf-font-comment-face 'font-lock-comment-face + nil) + (twelf-font-create-face 'twelf-font-percent-key-face 'default "Plum") + (twelf-font-create-face 'twelf-font-decl-face 'default "Orange") + (twelf-font-create-face 'twelf-font-parm-face 'default "Orange") + (twelf-font-create-face 'twelf-font-fvar-face 'default "SpringGreen") + (twelf-font-create-face 'twelf-font-evar-face 'default "Aquamarine")) + (t + (twelf-font-create-face 'twelf-font-keyword-face 'default nil) + (twelf-font-create-face 'twelf-font-comment-face 'font-lock-comment-face + nil) + (twelf-font-create-face 'twelf-font-percent-key-face 'default "MediumPurple") + (twelf-font-create-face 'twelf-font-decl-face 'default "FireBrick") + (twelf-font-create-face 'twelf-font-parm-face 'default "Green4") + (twelf-font-create-face 'twelf-font-fvar-face 'default "Blue1") + (twelf-font-create-face 'twelf-font-evar-face 'default "Blue4"))) + +;; Note that the order matters! + +(defvar twelf-font-patterns + '( + ;; delimited comments, perhaps should use different font + ;;("%{" "}%" comment) + (twelf-font-find-delimited-comment . twelf-font-comment-face) + ;; single-line comments + ;; replace \\W by \\s- for whitespace? + ("%\\W.*$" 0 twelf-font-comment-face) + ;; %keyword declarations + ("\\(%infix\\|%prefix\\|%prefix\\|%postfix\\|%name\\|%solve\\|%query\\|%mode\\|%terminates\\|%theorem\\|%prove\\).*$" + 1 twelf-font-percent-key-face nil) + ;; keywords, omit punctuations for now. + ("\\(\\<<-\\>\\|\\<->\\>\\|\\<type\\>\\|\\<=\\>\\|\\<_\\>\\)" + ;; for LLF, no punctuation marks +;;"\\(\\<<-\\>\\|\\<->\\>\\|\\<o-\\>\\|\\<-o\\>\\|\\<<T>\\>\\|\\<&\\>\\|\\^\\|()\\|\\<type\\>\\|\\<sigma\\>\\)" + ;; for LLF, with punctuation marks + ;;"\\([][:.(){},]\\|\\<<-\\>\\|\\<->\\>\\|\\<o-\\>\\|\\<-o\\>\\|\\<<T>\\>\\|\\<&\\>\\|\\^\\|()\\|\\<type\\>\\|\\<sigma\\>\\)" + ;; for Elf, no punction marks + ;;"\\(\\<<-\\>\\|\\<->\\>\\|\\<type\\>\\|\\<sigma\\>\\)" + ;; for Elf, including punctuation marks + ;;"\\([][:.(){}]\\|\\<<-\\>\\|\\<->\\>\\|\\<type\\>\\|\\<sigma\\>\\)" + . twelf-font-keyword-face) + ;; declared constants + (twelf-font-find-decl . twelf-font-decl-face) + ;; parameters + (twelf-font-find-parm . twelf-font-parm-face) + ;; quantified existentials + (twelf-font-find-evar . twelf-font-evar-face) + ;; lower-case identifiers (almost = constants) + ;;("\\<\\([a-z!&$^+/<=>?@~|#*`;,]\\|\\-\\|\\\\\\)\\w*\\>" + ;; nil black) + ;; upper-case identifiers (almost = variables) + ("\\<[A-Z_]\\w*\\>" . twelf-font-fvar-face) + ;; numbers and quoted identifiers omitted for now + ) + "Highlighting patterns for Twelf mode. +This generally follows the syntax of the FONT-LOCK-KEYWORDS variable, +but allows an arbitrary function to be called instead of just +regular expressions." + ) + +(defun twelf-font-fontify-decl () + "Fontifies the current Twelf declaration." + (interactive) + (let* ((region (twelf-current-decl)) + (start (nth 0 region)) + (end (nth 1 region))) + (save-excursion + (font-lock-unfontify-region start end) + (twelf-font-fontify-region start end)))) + +(defun twelf-font-fontify-buffer () + "Fontitifies the current buffer as Twelf code." + (interactive) + (if (not twelf-config-mode) + (save-excursion + (font-lock-unfontify-region (point-min) (point-max)) ; t optional in XEmacs + (twelf-font-fontify-region (point-min) (point-max))))) + +(defun twelf-font-unfontify () + "Removes fontification from current buffer." + (interactive) + (font-lock-unfontify-region (point-min) (point-max))) ; t optional in XEmacs + +(defvar font-lock-message-threshold 6000) ; in case we are running FSF Emacs + +(defun twelf-font-fontify-region (start end) + "Go through TWELF-FONT-PATTERNS, fontifying according to given functions" + (save-restriction + (narrow-to-region start end) + (if (and font-lock-verbose + (>= (- end start) font-lock-message-threshold)) + (message "Fontifying %s... (semantically...)" (buffer-name))) + (let ((patterns twelf-font-patterns) + (case-fold-search nil) ; in Twelf, never case-fold + (modified (buffer-modified-p)) ; for FSF Emacs 19 + pattern + fun-or-regexp + instructions + face + match-index + allow-overlap-p + region) + (while patterns + (setq pattern (car patterns)) + (setq patterns (cdr patterns)) + (goto-char start) + (cond ((stringp pattern) + (setq match-index 0) + (setq face 'font-lock-keyword-face) + (setq allow-overlap-p nil)) + ((listp pattern) + (setq fun-or-regexp (car pattern)) + (setq instructions (cdr pattern)) + (cond ((integerp instructions) + (setq match-index instructions) + (setq face 'font-lock-keyword-face) + (setq allow-overlap-p nil)) + ((symbolp instructions) + (setq match-index 0) + (setq face instructions) + (setq allow-overlap-p nil)) + ((listp instructions) + (setq match-index (nth 0 instructions)) + (setq face (nth 1 instructions)) + (setq allow-overlap-p (nth 2 instructions))) + (t (error "Illegal font-lock-keyword instructions")))) + (t (error "Illegal font-lock-keyword instructions"))) + (cond ((symbolp fun-or-regexp) ; a function to call + (while + (setq region (funcall fun-or-regexp end)) + ;; END is limit of forward search, start at point + ;; and move point + ;; check whether overlap is permissible! + (twelf-font-highlight (car region) (cdr region) + face allow-overlap-p))) + ((stringp fun-or-regexp) ; a pattern to find + (while + (re-search-forward fun-or-regexp end t) + (goto-char (match-end match-index)) ; back-to-back font hack + (twelf-font-highlight (match-beginning match-index) + (match-end match-index) + face + allow-overlap-p))) + (t (error "Illegal font-lock-keyword instructions")))) + ;; For FSF Emacs 19: mark buffer not modified, if it wasn't before + ;; fontification. + (and (not modified) (buffer-modified-p) (set-buffer-modified-p nil)) + (if (and font-lock-verbose + (>= (- end start) font-lock-message-threshold)) + (message "Fontifying %s... done" (buffer-name)))))) + +(defun twelf-font-highlight (start end face allow-overlap-p) + "Highlight region between START and END with FONT. +If already highlighted and ALLOW-OVERLAP-P is nil, don't highlight." + (or (= start end) + ;;(if allow-overlap-p nil (font-lock-any-faces-p start (1- end))) + ;; different in XEmacs 19.16? font-lock-any-faces-p subtracts 1. + (if allow-overlap-p nil (font-lock-any-faces-p start end)) + (font-lock-set-face start end face))) + +(defun twelf-font-find-delimited-comment (limit) + "Find a delimited Twelf comment and return (START . END), nil if none." + (let ((comment-level nil) + (comment-start nil)) + (if (search-forward "%{" limit t) + (progn + (setq comment-start (- (point) 2)) + (setq comment-level 1) + (while (and (> comment-level 0) + (re-search-forward "\\(%{\\)\\|\\(}%\\)" + limit 'limit)) + (cond + ((match-beginning 1) (setq comment-level (1+ comment-level))) + ((match-beginning 2) (setq comment-level (1- comment-level))))) + (cons comment-start (point))) + nil))) + +;; doesn't work yet with LIMIT!!! +;; this should never be done in incremental-highlighting mode +(defun twelf-font-find-decl (limit) + "Find an Twelf constant declaration and return (START . END), nil if none." + (let (start + end + ;; Turn off error messages + (id (twelf-next-decl nil nil))) + ;; ignore limit for now because of global buffer restriction + (if (null id) ; (or (null id) (> (point) limit)) + nil + (skip-chars-backward *whitespace*) + (setq end (point)) + (beginning-of-line 1) + (setq start (point)) + (twelf-end-of-par) + (cons start end)))) + +(defun twelf-font-find-binder (var-pattern limit occ-face) + "Find Twelf binder whose bound variable matches var-pattern. +Returns (START . END) if found, NIL if there is none before LIMIT. +Binders have the form [x],[x:A],{y},{y:A}. +As a side-effect, it highlights all occurrences of the bound +variable using the variable OCC-FACE." + (let (start + end + par-end + scope-start + scope-end + word + (found nil)) + ;;; At the moment, ignore limit since restriction is done globally + ;; (save-restriction + ;; (narrow-to-region (point) limit) + (while (not found) + (skip-chars-forward "^[{%") + (while (looking-at *twelf-comment-start*) + (cond ((looking-at "%{") + (condition-case nil (forward-sexp 1) + (error (goto-char (point-max)))) + (or (eobp) (forward-char 1))) + (t + (end-of-line 1))) + (skip-chars-forward "^[{%")) + (if (eobp) + (setq found 'eob) + (forward-char 1) + (skip-chars-forward *whitespace*) + (if (looking-at var-pattern) + ;;"\\<\\w+\\>" + ;;"\\<[-a-z!&$^+/\\<=>?@~|#*`;,]\\w*\\>" + (setq found t)))) + (if (eq found 'eob) + nil + (setq start (match-beginning 0)) + (setq end (match-end 0)) + (setq word (buffer-substring start end)) + ;; find scope of quantifier + (twelf-end-of-par) + (setq par-end (point)) + (goto-char end) + (condition-case nil (up-list 1) ; end of quantifier + (error (goto-char par-end))) + (setq scope-start (min (point) par-end)) + (condition-case nil (up-list 1) ; end of scope + (error (goto-char par-end))) + (setq scope-end (min (point) par-end)) + (goto-char scope-start) + (while + ;; speed here??? + (search-forward-regexp (concat "\\<" (regexp-quote word) "\\>") + scope-end 'limit) + ;; Check overlap here!!! --- current bug if in comment + (font-lock-set-face (match-beginning 0) (match-end 0) + occ-face)) + (goto-char end) + (cons start end))) + ;;) + ) + +(defun twelf-font-find-parm (limit) + "Find bound Twelf parameters and return (START . END), NIL if none. +Also highlights all occurrences of the parameter. +For these purposes, a parameter is a bound, lower-case identifier." + (twelf-font-find-binder "\\<[-a-z!&$^+/\\<=>?@~|#*`;,]\\w*\\>" + limit 'twelf-font-parm-face)) + +(defun twelf-font-find-evar (limit) + "Find bound Twelf existential variable return (START . END), NIL if none. +Also highlights all occurrences of the existential variable. +For these purposes, an existential variable is a bound, upper-case identifier." + (twelf-font-find-binder "\\<[A-Z_]\\w*\\>" + limit 'twelf-font-evar-face)) + +; next two are now in twelf.el +;(define-key twelf-mode-map "\C-c\C-l" 'twelf-font-fontify-decl) +;(define-key twelf-mode-map "\C-cl" 'twelf-font-fontify-buffer) + + + + +(provide 'twelf-font) diff --git a/twelf/twelf-old.el b/twelf/twelf-old.el new file mode 100644 index 00000000..61b21745 --- /dev/null +++ b/twelf/twelf-old.el @@ -0,0 +1,2661 @@ +;; twelf-old.el Port of old Twelf Emacs mode +;; +;; Author: Frank Pfenning +;; Adapted for Proof General by David Aspinall <da@dcs.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 'auc-menu) + +;;;---------------------------------------------------------------------- +;;; 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-int 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-int (looked-at-string input 1)))) + ;;((string-match "^set\\s +trace\\s +\\([0-9]\\)+" input) + ;; (setq twelf-trace (string-to-int (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-int 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) + diff --git a/twelf/twelf.el b/twelf/twelf.el new file mode 100644 index 00000000..56f9341b --- /dev/null +++ b/twelf/twelf.el @@ -0,0 +1,58 @@ +;; twelf.el Proof General instance for Twelf +;; +;; Copyright (C) 2000 LFCS Edinburgh. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; +;; $Id$ +;; +;; + +(require 'proof-easy-config) ; easy configure mechanism + +(require 'twelf-font) ; font lock configuration +;; (require 'twelf-old) ; port of parts of old code + +(proof-easy-config + 'twelf "Twelf" + proof-prog-name "twelf-server" + proof-assistant-home-page "http://www.cs.cmu.edu/~twelf/" + proof-terminal-char ?\. + ;; FIXME: must also cope with single line comments beginning with % + proof-comment-start "%{" + proof-comment-end "}%" + proof-comment-start-regexp "%[%{\t\n\f]" + proof-comment-end "" + ;; FIXME: these don't apply? + proof-goal-command-regexp "^%theorem" + proof-save-command-regexp "" ;; FIXME: empty? + proof-goal-with-hole-regexp "^%theorem\w-+\\(.*\\)\w-+:" + proof-save-with-hole-regexp "" ;; FIXME + ;; proof-non-undoables-regexp "undo\\|back" + proof-goal-command "%theorem %s." + proof-save-command "%prove " + ;; proof-kill-goal-command "Goal \"PROP no_goal_set\";" + +;; proof-showproof-command "pr()" +;; proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-auto-multiple-files t + proof-shell-cd-cmd "Twelf.OS.chDir \"%s\";" +;; proof-shell-prompt-pattern "[ML-=#>]+>? " +;; proof-shell-interrupt-regexp "Interrupt" +;; proof-shell-start-goals-regexp "Level [0-9]" +;; proof-shell-end-goals-regexp "val it" + + ;; FIXME! + ;; proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? " + proof-shell-error-regexp "%% ABORT %%" + proof-shell-quit-cmd "quit." + proof-shell-restart-cmd "reset." + + ;; proof-shell-init-cmd + ;; "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" + ;; proof-shell-proof-completed-regexp "^No subgoals!" + ;; proof-shell-eager-annotation-start + ;;"^\\[opening \\|^###\\|^Reading") + ) + +(provide 'twelf)
\ No newline at end of file |