[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 1931c8c 01/13: Remove Twelf support
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general 1931c8c 01/13: Remove Twelf support |
|
Date: |
Thu, 25 Nov 2021 10:57:57 -0500 (EST) |
branch: elpa/proof-general
commit 1931c8c7970afc6d2b80eb966ca9d08da752e736
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>
Remove Twelf support
---
Makefile | 4 +-
README.md | 3 +-
doc/ProofGeneral.texi | 9 +-
generic/proof-site.el | 1 -
proof-general.el | 4 +-
twelf/README | 27 -
twelf/example.elf | 64 --
twelf/twelf-font.el | 444 ---------
twelf/twelf-old.el | 2660 -------------------------------------------------
twelf/twelf.el | 209 ----
10 files changed, 14 insertions(+), 3411 deletions(-)
diff --git a/Makefile b/Makefile
index 4db14a0..b51aaef 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ PREFIX=$(DESTDIR)/usr
DEST_PREFIX=$(DESTDIR)/usr
# subdirectories for provers: to be compiled and installed
-PROVERS=acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml
pgshell phox twelf
+PROVERS=acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml
pgshell phox
# generic lisp code: to be compiled and installed
OTHER_ELISP=generic lib
@@ -58,7 +58,7 @@ ELISP_EXTRAS=
EXTRA_DIRS = images
DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER
doc/*.pdf
-DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l
pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
+DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l
pgshell/*.pgsh phox/*.phx plastic/*.lf
DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS
BATCHEMACS=${EMACS} --batch --no-site-file -q
diff --git a/README.md b/README.md
index ab9da9c..558a144 100644
--- a/README.md
+++ b/README.md
@@ -140,8 +140,9 @@ instances are no longer maintained nor available in the
MELPA package:
* Legacy support of
[Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/) and
[LEGO](http://www.dcs.ed.ac.uk/home/lego)
-* Experimental support of: CCC, ACL2, HOL98, Hol-Light, Lambda-Clam, Shell,
Twelf
+* Experimental support of: CCC, ACL2, HOL98, Hol-Light, Lambda-Clam, Shell
* Obsolete instances: Demoisa, Lambda-Clam, Plastic
+* Removed instances: Twelf
A few example proofs are included in each prover subdirectory.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index b55b12d..14bc95f 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -194,6 +194,7 @@ other documentation, system downloads, etc.
@menu
+* News for Version 4.5::
* News for Version 4.4::
* News for Version 4.3::
* News for Version 4.2::
@@ -203,6 +204,13 @@ other documentation, system downloads, etc.
* Credits::
@end menu
+@node News for Version 4.5
+@unnumberedsec News for Version 4.5
+@cindex news
+
+The old code for the support of the following systems have been
+removed: Twelf.
+
@node News for Version 4.4
@unnumberedsec News for Version 4.4
@cindex news
@@ -515,7 +523,6 @@ script file for your proof assistant, for example:
@item HOL98 @tab @file{.sml} @tab @code{hol98-mode}
@item HOL Light @tab @file{.ml} @tab @code{hol-light-mode}
@item ACL2 @tab @file{.acl2} @tab @code{acl2-mode}
-@item Twelf @tab @file{.elf} @tab @code{twelf-mode}
@item Plastic @tab @file{.lf} @tab @code{plastic-mode}
@item Lambda-CLAM @tab @file{.lcm} @tab @code{lclam-mode}
@item CCC @tab @file{.ccc} @tab @code{ccc-mode}
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 74bdaea..e6dd3e3 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -66,7 +66,6 @@
;; (hol98 "HOL" "sml")
;; (acl2 "ACL2" "acl2")
- ;; (twelf "Twelf" "elf")
;; (plastic "Plastic" "lf") ; obsolete
;; (lclam "Lambda-CLAM" "lcm") ; obsolete
;; (demoisa "Isabelle Demo" "ML") ; obsolete
diff --git a/proof-general.el b/proof-general.el
index 425ee60..b72509b 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -3,7 +3,7 @@
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2019 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
@@ -81,7 +81,7 @@
;; FIXME: These dirs used to not be listed, but I needed to add
;; them for the compilation to succeed for me. --Stef
;; These dirs are now obsolete and not published on MELPA. --Erik
- ;; "isar" "lego" "twelf" "obsolete/plastic"
+ ;; "isar" "lego" "obsolete/plastic"
)))
(dolist (dir byte-compile-directories)
(add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))
diff --git a/twelf/README b/twelf/README
deleted file mode 100644
index 2d91f55..0000000
--- a/twelf/README
+++ /dev/null
@@ -1,27 +0,0 @@
-Twelf Proof General, for Twelf.
-
-Written by David Aspinall.
-
-Status: not officially supported yet
-Maintainer: volunteer required
-Twelf version: Twelf 1.2 (and later, I hope)
-Twelf homepage: http://www.twelf.org
-
-========================================
-
-
-This is a "technology demonstration" of Proof General for Twelf.
-
-It has basic script management support, with some support for
-decoration taken from the present Twelf Emacs mode.
-
-There is support for X Symbol, but not using a proper token language,
-and it seems fairly broken because Twelf's syntax highlighting
-doesn't work properly with font lock.
-
-I have written this in the hope that somebody from the Twelf community
-will adopt it, maintain and improve it, and thus turn it into a proper
-instantiation of Proof General.
-
-$Id$
-
diff --git a/twelf/example.elf b/twelf/example.elf
deleted file mode 100644
index b428173..0000000
--- a/twelf/example.elf
+++ /dev/null
@@ -1,64 +0,0 @@
-%%%
-%%% Example script for Twelf Proof General.
-%%%
-%%% $Id$
-%%%
-
-%%% Rather than a proof this file is just a signature,
-%%% bunch of declarations. Would be nice to have something
-%%% closer to other systems for pedagogical purposes...
-%%% (i.e. proving commutativity of conjunction in ND fragment
-%%% of this logic)
-
-%%% Intuitionistic propositional calculus
-%%% Positive fragment with implies, and, true.
-%%% Two formulations here: natural deduction and Hilbert-style system.
-%%% Author: Frank Pfenning
-
-% Type of propositions.
-o : type.
-%name o A.
-
-% Syntax: implication, plus a few constants.
-=> : o -> o -> o. %infix right 10 =>.
-& : o -> o -> o. %infix right 11 &.
-true : o.
-
-% Provability.
-|- : o -> type. %prefix 9 |-.
-%name |- P.
-
-% Axioms.
-K : |- A => B => A.
-S : |- (A => B => C) => (A => B) => A => C.
-ONE : |- true.
-PAIR : |- A => B => A & B.
-LEFT : |- A & B => A.
-RIGHT : |- A & B => B.
-
-% Inference Rule.
-MP : |- A => B -> |- A -> |- B.
-
-% Natural Deduction.
-
-! : o -> type. %prefix 9 !.
-%name ! D.
-
-trueI : ! true.
-andI : ! A -> ! B -> ! A & B.
-andEL : ! A & B -> ! A.
-andER : ! A & B -> ! B.
-impliesI : (! A -> ! B) -> ! A => B.
-impliesE : ! A => B -> ! A -> ! B.
-
-% Normal deductions (for faster search)
-!^ : o -> type.
-!v : o -> type.
-
-trueI^ : !^ true.
-andI^ : !^ A -> !^ B -> !^ (A & B).
-andEvL : !v (A & B) -> !v A.
-andEvR : !v (A & B) -> !v B.
-impI^ : (!v A -> !^ B) -> !^ (A => B).
-impEv : !v (A => B) -> !^ A -> !v B.
-close : !v A -> !^ A.
diff --git a/twelf/twelf-font.el b/twelf/twelf-font.el
deleted file mode 100644
index 44e5468..0000000
--- a/twelf/twelf-font.el
+++ /dev/null
@@ -1,444 +0,0 @@
-;; 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 <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
-;;
-;;
-
-(require 'font-lock)
-
-;; FIXME da: integrate with PG's face mechanism?
-;; (but maybe keep twelf faces to help users)
-;; Also should add font locking.
-
-;; FIXME da: the twelf faces don't work with PG's
-;; background colouring, why?
-
-
-;; 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 ?\')
-
-;; 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)
- (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)
-
-
-;;;
-;;;
-;;; This comes from twelf-old.el but is needed for fontification,
-;;;
-;;; Perhaps some of these parsing functions will need reusing
-;;; for sending input to server properly?
-;;;
-
-;;; FIXME: some of names need fixing for safe conventions.
-
-(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-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))
-
-(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 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)))))
-
-
-(provide 'twelf-font)
diff --git a/twelf/twelf-old.el b/twelf/twelf-old.el
deleted file mode 100644
index 62763ba..0000000
--- a/twelf/twelf-old.el
+++ /dev/null
@@ -1,2660 +0,0 @@
-;; twelf-old.el Port of old Twelf Emacs mode
-;;
-;; Author: Frank Pfenning
-;; Adapted for Proof General by David Aspinall <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
-;;
-;;
-
-;; FIXME: have copied over directly!
-
-;;; Modes and utilities for Twelf programming. This package supports (1)
-;;; editing Twelf source files with reasonable indentation, (2) managing
-;;; configurations of Twelf source files, including TAGS tables, (3)
-;;; communication with an inferior Twelf server to type-check and execute
-;;; declarations and queries, (4) interaction with an inferior Twelf process
-;;; in SML.
-;;;
-;;; For documentation, type C-h m in Twelf mode, or see the function
-;;; twelf-mode below
-;;;
-;;; Author: Frank Pfenning
-;;; Thu Oct 7 19:48:50 1993 (1.0 created)
-;;; Fri Jan 6 09:06:38 1995 (2.0 major revision)
-;;; Tue Jun 16 15:49:31 1998 (3.0 major revision)
-;;;
-;;;======================================================================
-;;; For the `.emacs' file (copied from init.el)
-;;;======================================================================
-;;;
-;;; ;; Tell Emacs where the Twelf libraries are.
-;;; (setq load-path
-;;; (cons "/afs/cs/project/twelf/research/twelf/emacs" load-path))
-;;;
-;;; ;; Autoload libraries when Twelf-related major modes are started.
-;;; (autoload 'twelf-mode "twelf" "Major mode for editing Twelf source." t)
-;;; (autoload 'twelf-server "twelf" "Run an inferior Twelf server." t)
-;;; (autoload 'twelf-sml "twelf" "Run an inferior Twelf-SML process." t)
-;;;
-;;; ;; Switch buffers to Twelf mode based on filename extension,
-;;; ;; which is one of .elf, .quy, .thm, or .cfg.
-;;; (setq auto-mode-alist
-;;; (cons '("\\.elf$" . twelf-mode)
-;;; (cons '("\\.quy$" . twelf-mode)
-;;; (cons '("\\.thm$" . twelf-mode)
-;;; (cons '("\\.cfg$" . twelf-mode)
-;;; auto-mode-alist)))))
-;;;
-;;; ;; Default Twelf server program location
-;;; (setq twelf-server-program
-;;; "/afs/cs/project/twelf/research/twelf/bin/twelf-server")
-;;;
-;;; ;; Default Twelf SML program location
-;;; (setq twelf-sml-program
-;;; "/afs/cs/project/twelf/misc/smlnj/bin/sml-cm")
-;;;
-;;; ;; Default documentation location (in info format)
-;;; (setq twelf-info-file
-;;; "/afs/cs/project/twelf/research/twelf/doc/info/twelf.info")
-;;;
-;;; ;; Automatically highlight Twelf sources using font-lock
-;;; (add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer)
-;;;
-;;;======================================================================
-;;; Command Summary
-;;;======================================================================
-;;;
-;;; Quick summary of Twelf mode, generated from C-h b:
-;;;
-;;; --- Editing Commands ---
-;;; TAB twelf-indent-line
-;;; DEL backward-delete-char-untabify
-;;; M-C-q twelf-indent-decl
-;;;
-;;; --- Type Checking ---
-;;; C-c C-c twelf-save-check-config
-;;; C-c C-s twelf-save-check-file
-;;; C-c C-d twelf-check-declaration
-;;; C-c c twelf-type-const
-;;; C-c C-u twelf-server-display
-;;;
-;;; --- Error Tracking ---
-;;; C-c ` twelf-next-error
-;;; C-c = twelf-goto-error
-;;;
-;;; --- Syntax Highlighting ---
-;;; C-c C-l twelf-font-fontify-decl
-;;; C-c l twelf-font-fontify-buffer
-;;;
-;;; --- Server State ---
-;;; C-c < twelf-set
-;;; C-c > twelf-get
-;;; C-c C-i twelf-server-interrupt
-;;; M-x twelf-server
-;;; M-x twelf-server-configure
-;;; M-x twelf-server-quit
-;;; M-x twelf-server-restart
-;;; M-x twelf-server-send-command
-;;;
-;;; --- Timers ---
-;;; M-x twelf-timers-reset
-;;; M-x twelf-timers-show
-;;; M-x twelf-timers-check
-;;;
-;;; --- Tags (standard Emacs etags package) ---
-;;; M-x twelf-tag
-;;; M-. find-tag (standard binding)
-;;; C-x 4 . find-tag-other-window (standard binding)
-;;; C-c q tags-query-replace (Twelf mode binding)
-;;; C-c s tags-search (Twelf mode binding)
-;;; M-, tags-loop-continue (standard binding)
-;;; visit-tags-table, list-tags, tags-apropos
-;;;
-;;; --- Communication with inferior Twelf-SML process (not Twelf Server) ---
-;;; M-x twelf-sml
-;;; C-c C-e twelf-sml-send-query
-;;; C-c C-r twelf-sml-send-region
-;;; C-c RET twelf-sml-send-newline
-;;; C-c ; twelf-sml-send-semicolon
-;;; C-c d twelf-sml-cd
-;;; M-x twelf-sml-quit
-;;;
-;;; --- Variables ---
-;;; twelf-indent amount of indentation for nested Twelf expressions
-;;;
-;;;======================================================================
-;;; Some Terminology
-;;;======================================================================
-;;;
-;;; Twelf Server --- an inferior process that services requests to type-check,
-;;; load, or execute declarations and queries. It is usually attached to the
-;;; buffer *twelf-server*. Requests are generated by Emacs from user commands,
-;;; or may be typed directly into the Twelf server buffer.
-;;;
-;;; Current configuration --- A configuration is an ordered list of
-;;; Twelf source files in dependency order. It is usually initialized
-;;; and maintained in a file sources.cfg. The current configuration is
-;;; also the bases for the TAGS file created by twelf-tags. This allows
-;;; quick jumping to declaration sites for constants, or to apply
-;;; searches or replacements to all files in a configuration.
-;;;
-;;; Current Twelf declaration --- When checking individual declarations
-;;; Emacs must extract it from the current buffer and then send it to
-;;; the server. This is necessarily based on a heuristic, since Emacs
-;;; does not know enough in order to parse Twelf source properly in all
-;;; cases, but it knows the syntax for comments, Twelf identifiers, and
-;;; matching delimiters. Search for the end or beginning of a
-;;; declaration is always limited by double blank lines in order to be
-;;; more robust (in case a period is missing at the end of a
-;;; declaration). If the point falls between declarations, the
-;;; declaration after the point is considered current.
-;;;
-;;; Twelf-SML --- During development or debugging of the Twelf
-;;; implementation itself it is often useful to interact with SML, the
-;;; language in which Twelf is implementated, rather than using an Twelf
-;;; server. This is an inferior SML process which may run a Twelf
-;;; query interpreter.
-;;;
-;;;======================================================================
-;;; Change Log
-;;;======================================================================
-;;;
-;;; Thu Jun 3 14:51:35 1993 -fp
-;;; Added variable display-elf-queries. If T (default) redisplays Elf
-;;; buffer after a query has been sent. Delays one second after sending
-;;; the query which is rather arbitrary.
-;;; Wed Jun 30 19:57:58 1993
-;;; - Error messages in the format line0.col0-line1.col1 can now be parsed.
-;;; - Error from std_in, either interactive or through elf-send-query
-;;; can now be tracked.
-;;; - Added simple directory tracking and function elf-cd, bound to C-c d.
-;;; - improved filename completion in Elf mode under Lucid Emacs.
-;;; - replaced tail recursion in elf-indent-line by a while loop.
-;;; - changed elf-input-filter to ignore one character inputs.
-;;; - elf-error-marker is now updated on every interactive input or send.
-;;; - added commands elf-send-newline, bound to C-c RET
-;;; and elf-send-semicolon, bound to C-c ;.
-;;; These are useful when sending queries from a buffer with examples.
-;;; Fri Sep 3 15:02:10 1993
-;;; Changed definition of elf-current-paragraph so that it recognizes
-;;; individual declarations within a traditional ``paragraph'' (separated
-;;; by blank lines).
-;;; Fri Oct 22 10:05:08 1993
-;;; Changed elf-send-query to ensure that the Elf process expects a query
-;;; If the Elf process is at the SML prompt, it starts a top level.
-;;; If the Elf process is waiting after printing an answer substitution,
-;;; it sends a RET.
-;;; This is based on a heuristic analysis of the contents of the Elf buffer.
-;;; Fri Dec 16 15:27:14 1994
-;;; Changed elf-error-marker to elf-error-pos, since it moved in undesirable
-;;; ways in Emacs 19.
-;;; Fri Jan 6 09:06:54 1995
-;;; Major revision: incorporating elf-server.el and elf-tag.el
-;;; Thu Jan 12 14:31:36 1995
-;;; Finished major revision (version 2.0)
-;;; Sat Jun 13 12:14:34 1998
-;;; Renamed to Twelf and incorporated menus from elf-menu.el
-;;; Major revision for Twelf 1.2 release
-;;; Q: Improve tagging for %keyword declarations?
-;;; Thu Jun 25 08:52:41 1998
-;;; Finished major revision (version 3.0)
-;;; Fri Oct 2 11:06:15 1998
-;;; Added NT Emacs bug workaround
-
-(require 'comint)
-(require 'easymenu)
-
-;;;----------------------------------------------------------------------
-;;; User visible variables
-;;;----------------------------------------------------------------------
-
-(defvar twelf-indent 3
- "*Indent for Twelf expressions.")
-
-(defvar twelf-infix-regexp ":\\|\\<->\\>\\|\\<<-\\>\\|\\<=\\>"
- "*Regular expression to match Twelf infix operators.
-Match must exclude surrounding whitespace. This is used for indentation.")
-
-(defvar twelf-server-program "twelf-server"
- "*Default Twelf server program.")
-
-(defvar twelf-info-file "twelf.info"
- "*Default info file for Twelf.")
-
-(defvar twelf-server-display-commands nil
- "*If non-nil, the Twelf server buffer will be displayed after each command.
-Normally, the Twelf server buffer is displayed only after some selected
-commands or if a command is given a prefix argument.")
-
-(defvar twelf-highlight-range-function 'twelf-highlight-range-zmacs
- "*Function which highlights the range analyzed by the server.
-This is called for certain commands which apply to a subterm at point.
-You may want to change this for FSF Emacs, XEmacs and/or highlight packages.")
-
-(defvar twelf-focus-function 'twelf-focus-noop
- "*Function which focusses on the current declaration or query.
-This is called for certain commands which pick out (a part of) a declaration
-or query. You may want to change this for FSF Emacs, XEmacs and/or highlight
-packages.")
-
-(defvar twelf-server-echo-commands t
- "*If nil, Twelf server commands will not be echoed in the Twelf server
buffer.")
-
-(defvar twelf-save-silently nil
- "*If non-nil, modified buffers are saved without confirmation
-before `twelf-check-config' if they belong to the current configuration.")
-
-(defvar twelf-server-timeout 5
- "*Number of seconds before the server is considered delinquent.
-This is unsupported in some versions of Emacs.")
-
-(defvar twelf-sml-program "twelf-sml"
- "*Default Twelf-SML program.")
-
-(defvar twelf-sml-args '()
- "*Arguments to Twelf-SML program.")
-
-(defvar twelf-sml-display-queries t
- "*If nil, the Twelf-SML buffer will not be selected after a query.")
-
-(defvar twelf-mode-hook '()
- "List of hook functions to run when switching to Twelf mode.")
-
-(defvar twelf-server-mode-hook '()
- "List of hook functions to run when switching to Twelf Server mode.")
-
-(defvar twelf-config-mode-hook '()
- "List of hook functions to run when switching to Twelf Config minor mode.")
-
-(defvar twelf-sml-mode-hook '()
- "List of hook functions for Twelf-SML mode.")
-
-(defvar twelf-to-twelf-sml-mode '()
- "List of hook functions for 2Twelf-SML minor mode.")
-
-(defvar twelf-config-mode nil
- "Non-NIL means the Twelf Config minor mode is in effect.")
-
-;;;----------------------------------------------------------------------
-;;; Internal variables
-;;;----------------------------------------------------------------------
-
-(defvar *twelf-server-buffer-name* "*twelf-server*"
- "The default name for the Twelf server buffer.")
-
-(defvar *twelf-server-buffer* nil
- "The buffer with the Twelf server if one exists.")
-
-(defvar *twelf-server-process-name* "twelf-server"
- "Name of the Twelf server process.")
-
-(defvar *twelf-config-buffer* nil
- "The current Twelf configuration buffer if one exists.")
-
-(defvar *twelf-config-time* nil
- "The modification time of Twelf configuration file when read by the server.")
-
-(defvar *twelf-config-list* nil
- "The reversely ordered list with files in the current Twelf configuration.")
-
-(defvar *twelf-server-last-process-mark* 0
- "The process mark before the last command in the Twelf server buffer.")
-
-(defvar *twelf-last-region-sent* nil
- "Contains a list (BUFFER START END) identifying the last region sent
-to the Twelf server or Twelf-SML process for error tracking.
-If nil, then the last input was interactive.
-If t, then the last input was interactive, but has already been copied
-to the end of the Twelf-SML buffer.")
-
-(defvar *twelf-last-input-buffer* nil
- "Last buffer to which input was sent.
-This is used by the error message parser.")
-
-(defvar *twelf-error-pos* 0
- "Last error position in the server buffer.")
-
-(defconst *twelf-read-functions*
- '((nat . twelf-read-nat)
- (bool . twelf-read-bool)
- (limit . twelf-read-limit)
- (strategy . twelf-read-strategy))
- "Association between Twelf parameter types and their Emacs read functions.")
-
-(defconst *twelf-parm-table*
- '(("chatter" . nat)
- ("doubleCheck" . bool)
- ("Print.implicit" . bool)
- ("Print.depth" . limit)
- ("Print.length" . limit)
- ("Print.indent" . nat)
- ("Print.width" . nat)
- ("Prover.strategy" . strategy)
- ("Prover.maxSplit" . nat)
- ("Prover.maxRecurse" . nat))
- "Association between Twelf parameters and their types.")
-
-(defvar twelf-chatter 3
- "Chatter level in current Twelf server.
-Maintained to present reasonable menus.")
-
-;(defvar twelf-trace 0
-; "Trace level in current Twelf server.
-;Maintained to present reasonable menus.")
-
-(defvar twelf-double-check "false"
- "Current value of doubleCheck Twelf parameter.")
-
-(defvar twelf-print-implicit "false"
- "Current value of Print.implicit Twelf parameter.")
-
-(defconst *twelf-track-parms*
- '(("chatter" . twelf-chatter)
- ;("trace" . twelf-trace)
- ("doubleCheck" . twelf-double-check)
- ("Print.implicit" . twelf-print-implicit))
- "Association between Twelf parameters and Emacs tracking variables.")
-
-;;;----------------------------------------------------------------------
-;;; Basic key bindings
-;;;----------------------------------------------------------------------
-
-(defun install-basic-twelf-keybindings (map)
- "General key bindings for Twelf and Twelf Server modes."
- ;; Additional tag keybindings
- (define-key map "\C-cq" 'tags-query-replace)
- (define-key map "\C-cs" 'tags-search)
- ;; Server state
- (define-key map "\C-c<" 'twelf-set)
- (define-key map "\C-c>" 'twelf-get)
- ;; Error handling
- (define-key map "\C-c`" 'twelf-next-error)
- (define-key map "\C-c=" 'twelf-goto-error)
- ;; Proper indentation
- (define-key map "\e\C-q" 'twelf-indent-decl)
- (define-key map "\t" 'twelf-indent-line)
- (define-key map "\177" 'backward-delete-char-untabify)
- ;; Info documentation
- (define-key map "\C-c\C-h" 'twelf-info)
- )
-
-;;;----------------------------------------------------------------------
-;;; Twelf mode
-;;; This mode should be used for files with Twelf declarations,
-;;; usually *.elf, *.quy, or *.thm, and Twelf configuration files *.cfg
-;;;----------------------------------------------------------------------
-
-(defun install-twelf-keybindings (map)
- "Install the key bindings for the Twelf mode."
- (define-key map "\C-cl" 'twelf-font-fontify-buffer) ;autoload twelf-font
- (define-key map "\C-c\C-l" 'twelf-font-fontify-decl) ;autoload twelf-font
- (define-key map "\C-c\C-i" 'twelf-server-interrupt)
- (define-key map "\C-c\C-u" 'twelf-server-display)
- (define-key map "\C-cc" 'twelf-type-const)
- ;(define-key map "\C-ce" 'twelf-expected-type-at-point)
- ;(define-key map "\C-cp" 'twelf-type-at-point)
- ;(define-key map "\C-c." 'twelf-complete)
- ;(define-key map "\C-c?" 'twelf-completions-at-point)
- (define-key map "\C-c\C-d" 'twelf-check-declaration)
- (define-key map "\C-c\C-s" 'twelf-save-check-file)
- (define-key map "\C-c\C-c" 'twelf-save-check-config)
- )
-
-(defvar twelf-mode-map nil
- "The keymap used in Twelf mode.")
-
-(cond ((not twelf-mode-map)
- (setq twelf-mode-map (make-sparse-keymap))
- (install-basic-twelf-keybindings twelf-mode-map)
- (install-twelf-keybindings twelf-mode-map)))
-
-;;;----------------------------------------------------------------------
-;;; General editing and indentation
-;;;----------------------------------------------------------------------
-
-(defvar twelf-mode-syntax-table nil
- "The syntax table used in Twelf mode.")
-
-(defun set-twelf-syntax (char entry)
- (modify-syntax-entry char entry twelf-mode-syntax-table))
-(defun set-word (char) (set-twelf-syntax char "w "))
-(defun set-symbol (char) (set-twelf-syntax char "_ "))
-
-(defun map-string (func string)
- (if (string= "" string)
- ()
- (funcall func (string-to-char string))
- (map-string func (substring string 1))))
-
-(if twelf-mode-syntax-table
- ()
- (setq twelf-mode-syntax-table (make-syntax-table))
- ;; A-Z and a-z are already word constituents
- ;; For fontification, it would be better if _ and ' were word constituents
- (map-string 'set-word "!&$^+/<=>?@~|#*`;,-0123456789\\") ; word constituents
- (map-string 'set-symbol "_'") ; symbol constituents
- ;; Delimited comments are %{ }%, see 1234 below.
- (set-twelf-syntax ?\ " ") ; whitespace
- (set-twelf-syntax ?\t " ") ; whitespace
- (set-twelf-syntax ?% "< 14") ; comment begin
- (set-twelf-syntax ?\n "> ") ; comment end
- (set-twelf-syntax ?: ". ") ; punctuation
- (set-twelf-syntax ?. ". ") ; punctuation
- (set-twelf-syntax ?\( "() ") ; open delimiter
- (set-twelf-syntax ?\) ")( ") ; close delimiter
- (set-twelf-syntax ?\[ "(] ") ; open delimiter
- (set-twelf-syntax ?\] ")[ ") ; close delimiter
- (set-twelf-syntax ?\{ "(}2 ") ; open delimiter
- (set-twelf-syntax ?\} "){ 3") ; close delimiter
- ;; Actually, strings are illegal but we include:
- (set-twelf-syntax ?\" "\" ") ; string quote
- ;; \ is not an escape, but a word constituent (see above)
- ;;(set-twelf-syntax ?\\ "/ ") ; escape
- )
-
-(defconst *whitespace* " \t\n\f"
- "Whitespace characters to be skipped by various operations.")
-
-(defconst *twelf-comment-start* (concat "%[%{" *whitespace* "]")
- "Regular expression to match the start of a Twelf comment.")
-
-(defconst *twelf-id-chars* "a-z!&$^+/<=>?@~|#*`;,\\-\\\\A-Z_0-9'"
- "Characters that constitute Twelf identifiers.")
-
-(defun skip-twelf-comments-and-whitespace ()
- "Skip Twelf comments (single-line or balanced delimited) and white space."
- (skip-chars-forward *whitespace*)
- (while (looking-at *twelf-comment-start*)
- (cond ((looking-at "%{") ; delimited comment
- (condition-case nil (forward-sexp 1)
- (error (goto-char (point-max))))
- (or (eobp) (forward-char 1)))
- (t ; single-line comment
- (end-of-line 1)))
- (skip-chars-forward *whitespace*)))
-
-(defun twelf-end-of-par (&optional limit)
- "Skip to presumed end of current Twelf declaration.
-Moves to next period or blank line (whichever comes first)
-and returns t if period is found, nil otherwise.
-Skips over comments (single-line or balanced delimited).
-Optional argument LIMIT specifies limit of search for period."
- (if (not limit)
- (save-excursion
- (forward-paragraph 1)
- (setq limit (point))))
- (while (and (not (looking-at "\\."))
- (< (point) limit))
- (skip-chars-forward "^.%" limit)
- (cond ((looking-at *twelf-comment-start*)
- (skip-twelf-comments-and-whitespace))
- ((looking-at "%")
- (forward-char 1))))
- (cond ((looking-at "\\.")
- (forward-char 1)
- t)
- (t ;; stopped at limit
- nil)))
-
-(defun twelf-current-decl ()
- "Returns list (START END COMPLETE) for current Twelf declaration.
-This should be the declaration or query under or just before
-point within the nearest enclosing blank lines.
-If declaration ends in `.' then COMPLETE is t, otherwise nil."
- (let (par-start par-end complete)
- (save-excursion
- ;; Skip backwards if between declarations
- (if (or (eobp) (looking-at (concat "[" *whitespace* "]")))
- (skip-chars-backward (concat *whitespace* ".")))
- (setq par-end (point))
- ;; Move forward from beginning of decl until last
- ;; declaration before par-end is found.
- (if (not (bobp)) (backward-paragraph 1))
- (setq par-start (point))
- (while (and (twelf-end-of-par par-end)
- (< (point) par-end))
- (setq par-start (point)))
- ;; Now par-start is at end of preceding declaration or query.
- (goto-char par-start)
- (skip-twelf-comments-and-whitespace)
- (setq par-start (point))
- ;; Skip to period or consective blank lines
- (setq complete (twelf-end-of-par))
- (setq par-end (point)))
- (list par-start par-end complete)))
-
-(defun twelf-mark-decl ()
- "Marks current Twelf declaration and moves point to its beginning."
- (interactive)
- (let* ((par (twelf-current-decl))
- (par-start (nth 0 par))
- (par-end (nth 1 par)))
- (push-mark par-end)
- (goto-char par-start)))
-
-(defun twelf-indent-decl ()
- "Indent each line of the current Twelf declaration."
- (interactive)
- (let* ((par (twelf-current-decl))
- (par-start (nth 0 par))
- (par-end (nth 1 par)))
- (goto-char par-start)
- (twelf-indent-lines (count-lines par-start par-end))))
-
-(defun twelf-indent-region (from to)
- "Indent each line of the region as Twelf code."
- (interactive "r")
- (cond ((< from to)
- (goto-char from)
- (twelf-indent-lines (count-lines from to)))
- ((> from to)
- (goto-char to)
- (twelf-indent-lines (count-lines to from)))
- (t nil)))
-
-(defun twelf-indent-lines (n)
- "Indent N lines starting at point."
- (interactive "p")
- (while (> n 0)
- (twelf-indent-line)
- (forward-line 1)
- (setq n (1- n))))
-
-(defun twelf-comment-indent ()
- "Calculates the proper Twelf comment column.
-Currently does not deal specially with pragmas."
- (cond ((looking-at "%%%")
- 0)
- ((looking-at "%[%{]")
- (car (twelf-calculate-indent)))
- (t
- (skip-chars-backward " \t")
- (max (if (bolp) 0 (1+ (current-column))) comment-column))))
-
-(defun looked-at ()
- "Returns the last string matched against.
-Beware of intervening, even unsuccessful matches."
- (buffer-substring (match-beginning 0) (match-end 0)))
-
-(defun twelf-indent-line ()
- "Indent current line as Twelf code.
-This recognizes comments, matching delimiters, and standard infix operators."
- (interactive)
- (let ((old-point (point)))
- (beginning-of-line)
- (let* ((indent-info (twelf-calculate-indent))
- (indent-column (nth 0 indent-info))
- (indent-type (nth 1 indent-info))
- (indent-string (nth 2 indent-info)))
- (skip-chars-forward " \t") ; skip whitespace
- (let ((fwdskip (- old-point (point))))
- (cond ((looking-at "%%%")
- (twelf-indent-line-to 0 fwdskip)) ; %%% comment at column 0
- ((looking-at "%[%{]") ; delimited or %% comment
- (twelf-indent-line-to indent-column fwdskip))
- ((looking-at *twelf-comment-start*) ; indent single-line
comment
- (indent-for-comment)
- (forward-char -1))
- ((looking-at "%") ; %keyword declaration
- (twelf-indent-line-to indent-column fwdskip))
- ((looking-at twelf-infix-regexp) ; looking at infix operator
- (if (string= indent-string (looked-at))
- ;; indent string is the same as the one we are looking at
- (twelf-indent-line-to indent-column fwdskip)
- (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))
- ((eq indent-type 'delimiter) ; indent after delimiter
- (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip))
- ((eq indent-type 'limit) ; no delimiter or infix found.
- (twelf-indent-line-to indent-column fwdskip))
- ((eq indent-type 'infix)
- (twelf-indent-line-to (+ indent-column twelf-indent)
fwdskip)))))))
-
-(defun twelf-indent-line-to (indent fwdskip)
- "Indent current line to INDENT then skipping to FWDSKIP if positive.
-Assumes point is on the first non-whitespace character of the line."
- (let ((text-start (point))
- (shift-amount (- indent (current-column))))
- (if (= shift-amount 0)
- nil
- (beginning-of-line)
- (delete-region (point) text-start)
- (indent-to indent))
- (if (> fwdskip 0)
- (forward-char fwdskip))))
-
-(defun twelf-calculate-indent ()
- "Calculate the indentation and return a list (INDENT INDENT-TYPE STRING).
-INDENT is a natural number,
-INDENT-TYPE is 'DELIMITER, 'INFIX, or 'LIMIT, and
-STRING is the delimiter, infix operator, or the empty string, respectively."
- (save-excursion
- (let* ((par (twelf-current-decl))
- (par-start (nth 0 par))
- (par-end (nth 1 par))
- (par-complete (nth 2 par))
- (limit (cond ((> par-start (point)) (point))
- ((and (> (point) par-end) par-complete) par-end)
- (t par-start))))
- (twelf-dsb limit))))
-
-(defun twelf-dsb (limit)
- "Scan backwards from point to find opening delimiter or infix operator.
-This currently does not deal with comments or mis-matched delimiters.
-Argument LIMIT specifies bound for backwards search."
- (let ((result nil)
- (lparens 0) (lbraces 0) (lbrackets 0))
- (while (not result)
- (if (or (= lparens 1) (= lbraces 1) (= lbrackets 1))
- (setq result (list (current-column) 'delimiter (looked-at)))
- (if (re-search-backward (concat "[][{}()]\\|" twelf-infix-regexp)
- limit 'limit) ; return 'LIMIT if limit reached
- (let ((found (looked-at)))
- (cond
- ((string= found "(") (setq lparens (1+ lparens)))
- ((string= found ")") (setq lparens (1- lparens)))
- ((string= found "{") (setq lbraces (1+ lbraces)))
- ((string= found "}") (setq lbraces (1- lbraces)))
- ((string= found "[") (setq lbrackets (1+ lbrackets)))
- ((string= found "]") (setq lbrackets (1- lbrackets)))
- (t;; otherwise, we are looking at an infix operator
- (if (and (= lparens 0) (= lbraces 0) (= lbrackets 0))
- (setq result (list (current-column) 'infix found))
- nil)))) ; embedded - skip
- (setq result (list 0 'limit ""))))) ; reached the limit, no indent
- result))
-
-(defun twelf-mode-variables ()
- "Set up local variables for Twelf mode."
- (set-syntax-table twelf-mode-syntax-table)
- ;; Paragraphs are separated by blank lines or ^L.
- (make-local-variable 'paragraph-start)
- (setq paragraph-start "^[ \t\f]*$")
- (make-local-variable 'paragraph-separate)
- (setq paragraph-separate paragraph-start)
- (make-local-variable 'indent-line-function)
- (setq indent-line-function 'twelf-indent-line)
- (make-local-variable 'comment-start)
- (setq comment-start "%")
- (make-local-variable 'comment-start-skip)
- (setq comment-start-skip "%+{?[ \t]*")
- (make-local-variable 'comment-end)
- (setq comment-end "")
- (make-local-variable 'comment-column)
- (setq comment-column 40)
- ;; (make-local-variable 'parse-sexp-ignore-comments)
- ;; (setq parse-sexp-ignore-comments t)
- )
-
-(defun twelf-mode ()
- "Major mode for editing Twelf code.
-Tab indents for Twelf code.
-Delete converts tabs to spaces as it moves back.
-M-C-q indents all lines in current Twelf declaration.
-
-Twelf mode also provides commands to maintain groups of Twelf source
-files (configurations) and communicate with an Twelf server which
-processes declarations. It also supports quick jumps to the (presumed)
-source of error message that may arise during parsing or type-checking.
-
-Customisation: Entry to this mode runs the hooks on twelf-mode-hook.
-See also the hints for the .emacs file given below.
-
-Mode map
-========
-\\{twelf-mode-map}
-\\<twelf-mode-map>
-Overview
-========
-
-The basic architecture is that Emacs sends commands to an Twelf server
-which runs as an inferior process, usually in the buffer *twelf-server*.
-Emacs in turn interprets or displays the replies from the Twelf server.
-Since a typical Twelf application comprises several files, Emacs
-maintains a configuration in a file, usally called sources.cfg. This
-file contains a list of files, each on a separate line, in dependency
-order. The `%' character starts a comment line. A configuration is
-established with the command \\[twelf-server-configure].
-
-A new file is switched to Twelf mode if a file has extension `.elf',
-`.quy', `.thm' or `.cfg' and the `auto-mode-alist' is set correctly (see
-init.el).
-
-The files in the current configuration can be checked in sequence with
-\\[twelf-save-check-config], the current file with
-\\[twelf-save-check-file], individual declarations with
-\\[twelf-check-declaration]. These, like many other commands, take an
-optional prefix arguments which means to display the Twelf server buffer
-after the processing of the configuration, file, or declaration. If an
-error should arise during these or related operations a message is
-issued both in the server buffer and Emacs, and the command
-\\[twelf-next-error] visits the presumed source of the type error in a
-separate buffer.
-
-Summary of most common commands:
- M-x twelf-save-check-config \\[twelf-save-check-config] save, check & load
configuration
- M-x twelf-save-check-file \\[twelf-save-check-file] save, check & load
current file
- M-x twelf-check-declaration \\[twelf-check-declaration] type-check
declaration at point
- M-x twelf-server-display \\[twelf-server-display] display Twelf server
buffer
-
-It is important to remember that the commands to save and check
-a file or check a declaration may change the state of the global
-signature maintained in Twelf. After a number of changes it is usually
-a good idea to return to a clean slate with \\[twelf-save-check-config].
-
-Individual Commands
-===================
-
-Configurations, Files and Declarations
-
- twelf-save-check-config \\[twelf-save-check-config]
- Save its modified buffers and then check the current Twelf configuration.
- With prefix argument also displays Twelf server buffer.
- If necessary, this will start up an Twelf server process.
-
- twelf-save-check-file \\[twelf-save-check-file]
- Save buffer and then check it by giving a command to the Twelf server.
- With prefix argument also displays Twelf server buffer.
-
- twelf-check-declaration \\[twelf-check-declaration]
- Send the current declaration to the Twelf server process for checking.
- With prefix argument, subsequently display Twelf server buffer.
-
-Subterm at Point
-
- twelf-type-const \\[twelf-type-const]
- Display the type of the constant before point.
- Note that the type of the constant will be `absolute' rather than the
- type of the particular instance of the constant.
-
-Error Tracking
-
- twelf-next-error \\[twelf-next-error]
- Find the next error by parsing the Twelf server or Twelf-SML buffer.
-
- twelf-goto-error \\[twelf-goto-error]
- Go to the error reported on the current line or below.
-
-Server State
-
- twelf-set PARM VALUE \\[twelf-set]
- Sets the Twelf server parameter PARM to VALUE.
- Prompts for PARM when called interactively, using completion for legal
- parameters.
-
- twelf-get PARM \\[twelf-get]
- Print the current value the Twelf server parameter PARM.
-
- twelf-server-interrupt \\[twelf-server-interrupt]
- Interrupt the Twelf server-process.
-
- twelf-server \\[twelf-server]
- Start a Twelf server process in a buffer named *twelf-server*.
-
- twelf-server-configure \\[twelf-server-configure]
- Set the current configuration of the Twelf server.
-
- twelf-reset \\[twelf-reset]
- Reset the global signature in the Twelf server process.
-
- twelf-server-quit \\[twelf-server-quit]
- Kill the Twelf server process.
-
- twelf-server-restart \\[twelf-server-restart]
- Restarts server and re-initializes configuration.
- This is primarily useful during debugging of the Twelf server code or
- if the Twelf server is hopelessly wedged.
-
- twelf-server-send-command \\[twelf-server-send-command]
- Send arbitrary string to Twelf server.
-
-Tags (for other, M-x apropos tags or see `etags' documentation)
-
- twelf-tag \\[twelf-tag]
- Create tags file TAGS for current configuration.
- If current configuration is names CONFIGx, tags file will be named TAGx.
- Errors are displayed in the Twelf server buffer.
-
-Timers
-
- twelf-timers-reset \\[twelf-timers-reset]
- Reset Twelf timers.
-
- twelf-timers-show \\[twelf-timers-show]
- Show and reset Twelf timers.
-
- twelf-timers-check \\[twelf-timers-check]
- Show, but do not reset Twelf timers.
-
-Editing
-
- twelf-indent-decl \\[twelf-indent-decl]
- Indent each line in current declaration as Twelf code.
-
- twelf-indent-region \\[twelf-indent-region]
- Indent each line of the region as Twelf code.
-
-Minor Modes
-===========
-
-An associated minor modes is 2Twelf-SML (toggled with
-twelf-to-twelf-sml-mode). This means that we assume communication
-is an inferior Twelf-SML process and not a Twelf server.
-
-Related Major Modes
-===================
-
-Related major modes are Twelf Server (for the Twelf server buffer) and
-Twelf-SML (for an inferior Twelf-SML process). Both modes are based on
-the standard Emacs comint package and inherit keybindings for retrieving
-preceding input.
-
-Customization
-=============
-
-The following variables may be of general utility.
-
- twelf-indent amount of indentation for nested Twelf expressions
- twelf-mode-hook hook to run when entering Twelf mode
- twelf-server-program full pathname of Twelf server program
- twelf-server-mode-hook hook to run when entering Twelf server mode
- twelf-info-file name of Twelf info file with documentation
-
-The following is a typical section of a .emacs initialization file
-which can be found in the file init.el.
-
-(setq load-path (cons \"/afs/cs/project/twelf/research/twelf/emacs\"
load-path))
-
-(autoload 'twelf-mode \"twelf\" \"Major mode for editing Twelf source.\" t)
-(autoload 'twelf-server \"twelf\" \"Run an inferior Twelf server.\" t)
-(autoload 'twelf-sml \"twelf\" \"Run an inferior Twelf-SML process.\" t)
-
-(setq auto-mode-alist
- (cons '(\"\\.elf$\" . twelf-mode)
- (cons '(\"\\.quy$\" . twelf-mode)
- (cons '(\"\\.thm$\" . twelf-mode)
- (cons '(\"\\.cfg$\" . twelf-mode)
- auto-mode-alist)))))
-
-(setq twelf-server-program
- \"/afs/cs/project/twelf/research/twelf/bin/twelf-server\")
-
-(setq twelf-sml-program
- \"/afs/cs/project/twelf/misc/smlnj/bin/sml-cm\")
-
-(setq twelf-info-file
- \"/afs/cs/project/twelf/research/twelf/doc/info/twelf.info\")
-"
- (interactive)
- (kill-all-local-variables)
- (twelf-mode-variables)
- (use-local-map twelf-mode-map)
- (setq major-mode 'twelf-mode)
- (setq mode-name "Twelf")
- (twelf-config-mode-check)
- (twelf-add-menu) ; add Twelf menu to menubar
- ;; disable twelf-add-to-config-check: require explicit add-file
- ;; (twelf-add-to-config-check)
- (run-hooks 'twelf-mode-hook))
-
-;;;----------------------------------------------------------------------
-;;; Reading info file
-;;;----------------------------------------------------------------------
-
-(defun twelf-info (&optional file)
- "Enter Info, starting with the Twelf node
-Optional argument FILE specifies the info file.
-
-In interactive use, a prefix arguments directs this command to
-read a file name from the minibuffer."
- (interactive (if current-prefix-arg
- (list (read-file-name "Info file name: " nil nil t))))
- (info (or file twelf-info-file)))
-
-;;;----------------------------------------------------------------------
-;;; Error message parsing
-;;;----------------------------------------------------------------------
-
-(defconst twelf-error-regexp
- "^.+:[-0-9.:]+.* \\(Error\\|Warning\\):"
- "Regexp for matching Twelf error.")
-
-(defconst twelf-error-fields-regexp
- "^[-=? \t]*\\(.+\\):\
-\\([0-9]+\\)\\(\\.\\([0-9]+\\)\\)?\\(-\\([0-9]+\\)\\(\\.\\([0-9]+\\)\\)?\\)?\
-.+\\(Error\\|Warning\\):"
- "Regexp to extract fields of Twelf error.")
-
-(defconst twelf-error-decl-regexp
- "^[-=? \t]*\\(.+\\)::\\([^ \t\n]+\\) "
- "Regexp to extract filename and identifier from declaration error.")
-
-(defun looked-at-nth (n)
- (let ((b (match-beginning n))
- (e (match-end n)))
- (if (or (null b) (null e)) nil
- (buffer-substring (match-beginning n) (match-end n)))))
-
-(defun looked-at-nth-int (n)
- (let ((str (looked-at-nth n)))
- (if (null str) nil
- (string-to-number str))))
-
-(defun twelf-error-parser (pt)
- "Standard parser for Twelf errors.
-Returns a 5-element list (FILE START-LINE START-COL END-LINE END-COL)
-or (\"Local\" START-CHAR NIL END-CHAR NIL)."
- (save-excursion
- (goto-char pt)
- (re-search-forward twelf-error-fields-regexp)
- (list (looked-at-nth 1) ; file or "Local" or "stdIn"
- (looked-at-nth-int 2) ; start line or char
- (looked-at-nth-int 4) ; start column, if given, else nil
- (looked-at-nth-int 6) ; end line, if given, else nil or char
- (looked-at-nth-int 8) ; end column, if given, else nil
- )))
-
-(defun twelf-error-decl (pos)
- "Determines if the error is identified only by its declaration."
- (save-excursion
- (goto-char pos)
- (looking-at twelf-error-decl-regexp)))
-
-(defun twelf-mark-relative (line0 col0 line1 col1)
- "Mark error region if location is given relative to a buffer position."
- (if (not (= line0 1))
- (forward-line (1- line0)))
- ;; work around bug: from stdIn, first line is off by one.
- (forward-char (if (not (= line0 1)) (1- col0) (1- (1- col0))))
- ;; select region, if non-empty
- (cond ((not (null line1))
- (push-mark (point))
- (cond ((not (= line1 line0))
- (forward-line (- line1 line0))
- (forward-char (1- col1)))
- (t (forward-char (- col1 col0))))
- (exchange-point-and-mark)
- (funcall twelf-highlight-range-function (point) (mark)))))
-
-(defun twelf-mark-absolute (line0 col0 line1 col1)
- "Mark error region if location is given as absolute buffer position."
- (cond ((and line0 col0 line1 col1) ; line0.col0-line1.col1 range
- (goto-line line0)
- ;; don't use move-to-column since <tab> is 1 char to lexer
- (forward-char (1- col0))
- ;; select region, if non-empty
- (push-mark (point))
- (goto-line line1)
- (forward-char (1- col1))
- (exchange-point-and-mark)
- (funcall twelf-highlight-range-function (point) (mark)))
- ((and (null col0) (null col1)) ; char0-char1 range
- (goto-char line0)
- (push-mark (point))
- (goto-char line1)
- (exchange-point-and-mark)
- (funcall twelf-highlight-range-function (point) (mark)))
- ((and line0 col0) ; beginning line0.col0
- (goto-line line0)
- (forward-char (1- col0)))
- (line0 ; beginning char0
- (goto-char line0))
- (t (error "Unrecognized format for error location"))))
-
-(defun twelf-find-decl (filename id)
- "In FILENAME find probable declaration of ID."
- (if (not (file-readable-p filename))
- (error "Cannot read file %s" filename)
- (switch-to-buffer-other-window (find-file-noselect filename))
- (goto-char (point-min))
- (let ((done nil)
- decl-id)
- (while (not done)
- (setq decl-id (twelf-next-decl filename *twelf-last-input-buffer*))
- (if (not decl-id)
- (error "Declaration of %s not found in file %s." id filename)
- (setq done (string= decl-id id))
- (if (not done) (twelf-end-of-par)))))))
-
-(defun twelf-next-error ()
- "Find the next error by parsing the Twelf server or Twelf-SML buffer.
-Move the error message on the top line of the window;
-put the cursor at the beginning of the error source. If the
-error message specifies a range, the mark is placed at the end."
- (interactive)
- (let ((case-fold-search nil)
- (twelf-buffer (or *twelf-last-input-buffer*
- (error "Cannot determine process buffer with last
input")))
- error-begin)
- (pop-to-buffer twelf-buffer)
- (goto-char *twelf-error-pos*) ; go to last error
- (if (not (re-search-forward twelf-error-regexp (point-max) t))
- (error "No error message found.")
- (setq error-begin (match-beginning 0))
- (setq *twelf-error-pos* (point))
- (set-window-start (get-buffer-window twelf-buffer)
- (save-excursion (beginning-of-line) (point)))
- (if (twelf-error-decl error-begin)
- (twelf-find-decl (looked-at-nth 1) (looked-at-nth 2))
- (let* ((parse (twelf-error-parser error-begin))
- (file (nth 0 parse))
- (line0 (nth 1 parse))
- (col0 (nth 2 parse))
- (line1 (nth 3 parse))
- (col1 (nth 4 parse)))
- (cond ((equal file "stdIn")
- ;; Error came from direct input
- (cond ((null *twelf-last-region-sent*)
- ;; from last interactive input in the Twelf buffer
- (goto-char (point-max))
- (comint-previous-input 1)
- (setq *twelf-last-region-sent* t)
- (goto-char (process-mark
- (get-buffer-process twelf-buffer)))
- (twelf-mark-relative line0 col0 line1 col1))
- ((eq *twelf-last-region-sent* t)
- ;; from the waiting input in the Twelf buffer
- (goto-char (process-mark
- (get-buffer-process twelf-buffer)))
- (twelf-mark-relative line0 col0 line1 col1))
- (t
- ;; from a region sent from some buffer
- (let ((buf (nth 0 *twelf-last-region-sent*))
- (start (nth 1 *twelf-last-region-sent*)))
- (switch-to-buffer-other-window buf)
- (goto-char start)
- (twelf-mark-relative line0 col0 line1 col1)))))
- ((equal file "Local")
- ;; Error came from local input, usually to a server process
- ;; in this case the address relative, and expressed in
- ;; characters, rather than lines.
- (let ((local-buffer (nth 0 *twelf-last-region-sent*))
- ;; Local characters seem to be off by two
- (char0 (+ (nth 1 *twelf-last-region-sent*) (- line0 2)))
- (char1 (+ (nth 1 *twelf-last-region-sent*) (- line1 2))))
- (switch-to-buffer-other-window local-buffer)
- (goto-char char1)
- (push-mark)
- (goto-char char0)
- (exchange-point-and-mark)))
- ((file-readable-p file)
- ;; Error came from a source file
- (switch-to-buffer-other-window (find-file-noselect file))
- (twelf-mark-absolute line0 col0 line1 col1))
- (t
- (error (concat "Can't read file " file)))))))))
-
-(defun twelf-goto-error ()
- "Go to the error reported on the current line or below.
-Also updates the error cursor to the current line."
- (interactive)
- (pop-to-buffer (or *twelf-last-input-buffer*
- (error "Cannot determine process buffer with last input")))
- (beginning-of-line)
- (setq *twelf-error-pos* (point))
- (twelf-next-error))
-
-;;;----------------------------------------------------------------------
-;;; NT Emacs bug workaround
-;;;----------------------------------------------------------------------
-
-(defun twelf-convert-standard-filename (filename)
- "Convert FILENAME to form appropriate for Twelf Server of current OS."
- (cond ((eq system-type 'windows-nt)
- (while (string-match "/" filename)
- (setq filename (replace-match "\\" t t filename)))
- filename)
- (t (convert-standard-filename filename))))
-
-;;;----------------------------------------------------------------------
-;;; Communication with Twelf server
-;;;----------------------------------------------------------------------
-
-(defun string-member (x l)
- (if (null l) nil
- (or (string-equal x (car l)) (string-member x (cdr l)))))
-
-;(defun twelf-add-to-config-check ()
-; "Ask if current file should be added to the current Twelf configuration."
-; (let ((file-name (buffer-file-name)))
-; (if (and (not (string-member file-name *twelf-config-list*))
-; (not (null *twelf-config-buffer*))
-; (yes-or-no-p "Add to the current configuration? "))
-; (twelf-server-add-file file-name))))
-
-(defun twelf-config-proceed-p (file-name)
- "Ask if to proceed if FILE-NAME is not in current configuration."
- (if (and (not (string-member file-name *twelf-config-list*))
- (not (yes-or-no-p "File not in current configuration. Save? ")))
- nil
- t))
-
-(defun twelf-save-if-config (buffer)
- "Ask if BUFFER should be saved if in the current configuration.
-Always save if the variable `twelf-save-silently' is non-nil."
- (let ((file-name (buffer-file-name buffer)))
- (if (and (buffer-modified-p buffer)
- file-name
- (string-member file-name *twelf-config-list*))
- (if twelf-save-silently
- (save-buffer)
- (pop-to-buffer buffer)
- (if (yes-or-no-p (concat "Save " file-name "? "))
- (save-buffer))))))
-
-(defun twelf-config-save-some-buffers ()
- "Cycle through all buffers and save those in the current configuration."
- (mapcar 'twelf-save-if-config (buffer-list)))
-
-(defun twelf-save-check-config (&optional displayp)
- "Save its modified buffers and then check the current Twelf configuration.
-With prefix argument also displays Twelf server buffer.
-If necessary, this will start up an Twelf server process."
- (interactive "P")
- (let ((current-file-name (buffer-file-name)))
- (cond ((and current-file-name
- (not buffer-read-only)
- (buffer-modified-p)
- (twelf-config-proceed-p current-file-name))
- (save-buffer)))
- (save-excursion
- (twelf-config-save-some-buffers))
- (twelf-check-config displayp)))
-
-(defun twelf-check-config (&optional displayp)
- "Check the current Twelf configuration.
-With prefix argument also displays Twelf server buffer.
-If necessary, this will start up an Twelf server process."
- (interactive "P")
- (if (not *twelf-config-buffer*)
- (call-interactively 'twelf-server-configure))
- (twelf-server-sync-config)
- (twelf-focus nil nil)
- (twelf-server-send-command "Config.load")
- (twelf-server-wait displayp))
-
-(defun twelf-save-check-file (&optional displayp)
- "Save buffer and then check it by giving a command to the Twelf server.
-In Twelf Config minor mode, it reconfigures the server.
-With prefix argument also displays Twelf server buffer."
- (interactive "P")
- (save-buffer)
- (if twelf-config-mode
- (twelf-server-configure (buffer-file-name) "Server OK: Reconfigured")
- (let* ((save-file (buffer-file-name))
- (check-file (file-relative-name save-file (twelf-config-directory)))
- (check-file-os (twelf-convert-standard-filename check-file)))
- (twelf-server-sync-config)
- (twelf-focus nil nil)
- (twelf-server-send-command (concat "loadFile " check-file-os))
- (twelf-server-wait displayp))))
-
-(defun twelf-buffer-substring (start end)
- "The substring of the current buffer between START and END.
-The location is recorded for purposes of error parsing."
- (setq *twelf-last-region-sent* (list (current-buffer) start end))
- (buffer-substring start end))
-
-(defun twelf-buffer-substring-dot (start end)
- "The substring of the current buffer between START and END plus
-an end-of-input marker, `%.'. The location of the input is recorded
-for purposes of error parsing."
- (concat (twelf-buffer-substring start end) "%."))
-
-(defun twelf-check-declaration (&optional displayp)
- "Send the current declaration to the Twelf server process for checking.
-With prefix argument also displays Twelf server buffer."
- (interactive "P")
- (let* ((par (twelf-current-decl))
- (par-start (nth 0 par))
- (par-end (nth 1 par))
- (decl (twelf-buffer-substring-dot par-start par-end)))
- (twelf-focus par-start par-end)
- (twelf-server-send-command (concat "readDecl\n" decl))
- (twelf-server-wait displayp)))
-
-;(defun twelf-highlight-range (par-start par-end &optional offset)
-; "Set point and mark to encompass the range analyzed by the Twelf server."
-; (let* ((range (twelf-parse-range))
-; (range-start (nth 0 range))
-; (range-end (nth 1 range))
-; (offset (if (null offset) 0 offset)))
-; (if (and (integerp range-start) (integerp range-end))
-; (progn (goto-char (+ (- (+ par-start range-end) 2) offset))
-; (push-mark (- (+ par-start range-start) 2))
-; (funcall twelf-highlight-range-function (point) (mark))))))
-
-(defun twelf-highlight-range-zmacs (start end)
- "Highlight range as zmacs region. Assumes point and mark are set.
-Does nothing if function zmacs-activate-region is undefined."
- (if (fboundp 'zmacs-activate-region)
- (zmacs-activate-region)))
-
-(defun twelf-focus (&optional start end)
- "Focus on region between START and END as current declaration or query. If
-START and END are nil, then no focus exists. This intermediary just calls
-the appropriate function."
- (funcall twelf-focus-function start end))
-
-(defun twelf-focus-noop (start end)
- "This default focus function does nothing."
- ())
-
-;; Not yet available in Twelf 1.2 -fp
-
-;(defun twelf-type-at-point ()
-; "Display the type of the subterm at the point in the current Twelf decl.
-
-;The subterm at point is the smallest subterm whose printed representation
-;begins to the left of point and extends up to or beyond point. After this and
-;similar commands applicable to subterms, the current region (between mark and
-;point) is set to encompass precisely the selected subterm. In XEmacs,
-;it will thus be highlighted under many circumstances. In other versions
-;of Emacs \\[exchange-point-and-mark] will indicate the extent of the region.
-
-;The type computed for the subterm at point takes contextual information into
-;account. For example, if the subterm at point is a constant with implicit
-;arguments, the type displayed will be the instance of the constant (unlike
-;M-x twelf-type-const (\\[twelf-type-const]), which yields the absolute type
of a constant)."
-
-; (interactive)
-; (let* ((par (twelf-current-decl))
-; (par-start (nth 0 par))
-; (par-end (nth 1 par))
-; (decl (twelf-buffer-substring-dot par-start par-end)))
-; (twelf-focus par-start par-end)
-; (twelf-server-send-command
-; (concat "type-at "
-; (twelf-current-syncat) " "
-; (int-to-string (+ (- (point) par-start) 2)) "\n"
-; decl))
-; (twelf-server-wait t)
-; (twelf-highlight-range par-start par-end)))
-
-;(defun twelf-expected-type-at-point ()
-; "Display the type expected at the point in the current declaration.
-
-;This replaces the subterm at point by an underscore _ and determines
-;the type that _ would have to have for the whole declaration to be valid.
-;This is useful for debugging in places where inconsistent type constraints
-;have arisen. Error messages may be given, but will not be correctly
-;interpreted by Emacs, since the string sent to the server may be different
-;from the declaration in the buffer.
-
-;For a definition of the subterm at point, see function twelf-type-at-point."
-; (interactive)
-; (let* ((par (twelf-current-decl))
-; (par-start (nth 0 par))
-; (par-end (nth 1 par))
-; (par-initial-end nil)
-; (par-final-start nil)
-; modified-decl)
-; ;; (exp-present (not (looking-at (concat "[" *whitespace* "]"))))
-; (backward-sexp 1)
-; (setq par-initial-end (point))
-; (forward-sexp 1)
-; (setq par-final-start (point))
-; (setq modified-decl
-; (concat (twelf-buffer-substring par-start par-initial-end)
-; "_" (twelf-buffer-substring-dot par-final-start par-end)))
-; ;; Error messages here are not accurate. Nontheless:
-; (setq *twelf-last-region-sent* (list (current-buffer) par-start par-end))
-; (twelf-focus par-start par-end)
-; (twelf-server-send-command
-; (concat "type-at "
-; (twelf-current-syncat) " "
-; (int-to-string (1+ (+ (- par-initial-end par-start) 2))) "\n"
-; modified-decl))
-; (twelf-server-wait t)
-; (twelf-highlight-range par-start par-end
-; (1- (- par-final-start par-initial-end)))))
-
-;(defun twelf-parse-range ()
-; "Parse a range as returned by the Twelf server and return as a list."
-; (save-window-excursion
-; (let ((twelf-server-buffer (twelf-get-server-buffer)))
-; (set-buffer twelf-server-buffer)
-; (goto-char *twelf-server-last-process-mark*)
-; ;; We are now at the beginning of the output
-; (re-search-forward "^\\[\\([0-9]+\\),\\([0-9]+\\))")
-; (list (looked-at-nth-int 1) (looked-at-nth-int 2)))))
-
-(defun twelf-type-const ()
- "Display the type of the constant before point.
-Note that the type of the constant will be `absolute' rather than the
-type of the particular instance of the constant."
- (interactive)
- (let ((previous-point (point)))
- (skip-chars-backward *whitespace* (point-min))
- (skip-chars-forward *twelf-id-chars* (point-max))
- (let ((end-of-id (point)))
- (skip-chars-backward *twelf-id-chars* (point-min))
- (let ((c (if (= (point) end-of-id)
- ;; we didn't move. this should eventually become a
- ;; completing-read
- (read-string "Constant: ")
- (buffer-substring (point) end-of-id))))
- (twelf-server-send-command (concat "decl " c))
- (twelf-server-wait t) ; Wait for and display reply
- (goto-char previous-point)))))
-
-;; Unused? -fp
-;(defun twelf-backwards-parse-arglist ()
-; "Parse an argument list template as returned by the server."
-; (save-window-excursion
-; (let ((twelf-server-buffer (twelf-get-server-buffer)))
-; (set-buffer twelf-server-buffer)
-; (goto-char *twelf-server-last-process-mark*)
-; ;; Should be right at the beginning of the output.
-; ;; (re-search-forward "^arglist") ;
-; ;; (beginning-of-line 2)
-; (let ((arglist-begin (point)))
-; (skip-chars-forward "^." (point-max))
-; (buffer-substring arglist-begin (point))))))
-
-;; Not yet ported to Twelf 1.2
-;(defun twelf-show-region-in-window (start end)
-; "Change window parameters so it precisely shows the given region."
-; (enlarge-window (- (max (count-lines start end) window-min-height)
-; (window-height)))
-; (set-window-start (selected-window) start))
-
-;(defun twelf-show-menu ()
-; "Display the Twelf server buffer to show menu of possible completions."
-; (let ((old-buffer (current-buffer))
-; (twelf-server-buffer (twelf-get-server-buffer))
-; region-start region-end)
-; (switch-to-buffer-other-window twelf-server-buffer)
-; (goto-char *twelf-server-last-process-mark*)
-; (if (re-search-forward "-\\.$" (point-max) t)
-; (progn
-; (forward-char 1)
-; (setq region-start (point))
-; (if (re-search-forward "^-\\." (point-max) t)
-; (setq region-end (point))
-; (error "List of alternatives not terminated by -.")))
-; (error "No alternatives found."))
-; (twelf-show-region-in-window region-start region-end)
-; (switch-to-buffer-other-window old-buffer)))
-
-;(defun twelf-completions-at-point ()
-; "List the possible completions of the term at point based on type
information.
-
-;The possible completions are numbered, and the function twelf-complete
-;(\\[twelf-complete]) can be used subsequently to replace the term at point
with
-;one of the alternatives.
-
-;Above the display of the alternatives, the type of the subterm at
-;point is shown, since it is this type which is the basis for listing
-;the possible completions.
-
-;In the list alternatives, a variable X free in the remaining declaration
-;is printed ^X, and a bound variable x may be printed as !x. These marks
-;are intended to aid in the understanding of the alternatives, but
-;must be removed in case the alternative is copied literally into the
-;input declaration (as, for example, with the \\[twelf-complete] command)."
-; (interactive)
-; (let* ((par (twelf-current-decl))
-; (par-start (nth 0 par))
-; (par-end (nth 1 par))
-; (decl (twelf-buffer-substring-dot par-start par-end)))
-; (twelf-focus par-start par-end)
-; (twelf-server-send-command
-; (concat "complete-at "
-; (twelf-current-syncat) " "
-; (int-to-string (+ (- (point) par-start) 2)) "\n"
-; decl))
-; (twelf-server-wait nil)
-; (twelf-highlight-range par-start par-end)
-; (twelf-show-menu)))
-
-;(defun twelf-complete (n)
-; "Pick the alternative N from among possible completions.
-;This replaces the current region with the given pattern.
-;The list of completions must be generated with the command
-;twelf-completions-at-point (\\[twelf-completions-at-point])."
-; (interactive "NAlternative: ")
-; (let (start completion)
-; (save-excursion
-; (set-buffer (twelf-get-server-buffer))
-; (goto-char *twelf-server-last-process-mark*)
-; (if (not (re-search-forward (concat "^" (int-to-string n) "\\. ")
-; (point-max) t))
-; (error "No alternative %d found in Twelf server buffer." n))
-; (setq start (point))
-; (if (not (search-forward " ::" (point-max) t))
-; (error "List of completions not well-formed."))
-; (backward-char 3)
-; (setq completion (buffer-substring start (point))))
-; (delete-region (point) (mark))
-; (insert "(" completion ")")
-; (twelf-show-menu)))
-
-;;;----------------------------------------------------------------------
-;;; Twelf server mode (major mode)
-;;; This is for the buffer with the Twelf server process, to facilitate
-;;; direct interaction (which should rarely be necessary)
-;;;----------------------------------------------------------------------
-
-(defvar twelf-server-mode-map nil
- "The keymap used in twelf-server mode.")
-
-(cond ((not twelf-server-mode-map)
- (setq twelf-server-mode-map (copy-keymap comint-mode-map))
- (install-basic-twelf-keybindings twelf-server-mode-map)
- ;; C-c C-c is bound to twelf-save-check config in Twelf mode
- (define-key twelf-server-mode-map "\C-c\C-c" 'twelf-save-check-config)
- ;; Bind the function shadowed by the previous definition to C-c C-i
- (define-key twelf-server-mode-map "\C-c\C-i" 'comint-interrupt-subjob)
- ))
-
-(defconst twelf-server-cd-regexp "^\\s *OS\\.chDir\\s *\\(.*\\)"
- "Regular expression used to match cd commands in Twelf server buffer.")
-
-(defun looked-at-string (string n)
- "Substring of STRING consisting of Nth match."
- (substring string (match-beginning n) (match-end n)))
-
-(defun twelf-server-directory-tracker (input)
- "Checks input for cd commands and changes default directory in buffer.
-As a side effect, it resets *twelf-error-pos* and *twelf-last-region-sent*
-to indicate interactive input. Used as comint-input-filter-function in Twelf
-server buffer."
- (if (twelf-input-filter input)
- (setq *twelf-last-region-sent* nil))
- (setq *twelf-last-input-buffer* (current-buffer))
- (setq *twelf-error-pos* (marker-position (process-mark
(twelf-server-process))))
- (cond ((string-match twelf-server-cd-regexp input)
- (let ((expanded-dir (expand-dir (looked-at-string input 1))))
- (setq default-directory expanded-dir)
- (pwd)))
- ((string-match "^set\\s +chatter\\s +\\([0-9]\\)+" input)
- (setq twelf-chatter (string-to-number (looked-at-string input 1))))
- ;;((string-match "^set\\s +trace\\s +\\([0-9]\\)+" input)
- ;; (setq twelf-trace (string-to-number (looked-at-string input 1))))
- ((string-match "^set\\s-+\\(\\S-+\\)\\s-+\\(\\w+\\)" input)
- (if (assoc (looked-at-string input 1) *twelf-track-parms*)
- (set (cdr (assoc (looked-at-string input 1) *twelf-track-parms*))
- (looked-at-string input 2))))))
-
-(defun twelf-input-filter (input)
- "Function to filter strings before they are saved in input history.
-We filter out all whitespace and anything shorter than two characters."
- (and (not (string-match "\\`\\s *\\'" input))
- (> (length input) 1)))
-
-(defun twelf-server-mode ()
- "Major mode for interacting with an inferior Twelf server process.
-Runs twelf-server-mode-hook.
-
-The following commands are available:
-\\{twelf-server-mode-map}"
- (interactive)
- (kill-all-local-variables)
- ;; Initialize comint parameters
- (comint-mode)
- (setq comint-prompt-regexp "^") ;; no prompt
- (setq comint-input-filter 'twelf-input-filter)
- ;;changed for XEmacs 19.16
- ;;(setq comint-input-sentinel 'twelf-server-directory-tracker)
- (add-hook 'comint-input-filter-functions 'twelf-server-directory-tracker
- nil t)
- (twelf-mode-variables)
- ;; For sequencing through error messages:
- (make-local-variable '*twelf-error-pos*)
- (setq *twelf-error-pos* (point-max))
- ;; Set mode and keymap
- (setq major-mode 'twelf-server-mode)
- (setq mode-name "Twelf Server")
- (setq mode-line-process '(": %s"))
- (use-local-map twelf-server-mode-map)
- (twelf-server-add-menu) ; add Twelf Server menu
- ;; Run user specified hooks, if any
- (run-hooks 'twelf-server-mode-hook))
-
-;;;----------------------------------------------------------------------
-;;; Functions to support use of the Twelf server
-;;;----------------------------------------------------------------------
-
-(defun twelf-parse-config ()
- "Starting at point, parse a configuration file."
- (let ((filelist nil))
- (skip-chars-forward *whitespace*)
- (while (not (eobp)) ; end of buffer?
- (cond ((looking-at "%") ; comment through end of line
- (end-of-line))
- (t (let ((begin-point (point))) ; parse filename starting at point
- (skip-chars-forward (concat "^" *whitespace*))
- (let* ((file-name (buffer-substring begin-point (point)))
- (absolute-file-name
- (expand-file-name file-name default-directory)))
- (if (file-readable-p absolute-file-name)
- (setq filelist (cons absolute-file-name filelist))
- (error "File %s not readable." file-name))))))
- (skip-chars-forward *whitespace*))
- filelist))
-
-(defun twelf-server-read-config ()
- "Read the configuration and initialize *twelf-config-list*."
- (if (or (not (bufferp *twelf-config-buffer*))
- (null (buffer-name *twelf-config-buffer*)))
- (error "No current configuration buffer"))
- (set-buffer *twelf-config-buffer*)
- (goto-char (point-min))
- (twelf-parse-config))
-
-(defun twelf-server-sync-config ()
- "Synchronize the configuration file, buffer, and Twelf server."
- (if (or (not (bufferp *twelf-config-buffer*))
- (null (buffer-name *twelf-config-buffer*)))
- (error "No current configuration buffer"))
- (if (and twelf-config-mode
- (not (equal *twelf-config-buffer* (current-buffer)))
- (yes-or-no-p "Buffer is different from current configuration,
reconfigure server? "))
- (twelf-server-configure (buffer-file-name (current-buffer))
- "Server OK: Reconfigured"))
- (save-excursion
- (set-buffer *twelf-config-buffer*)
- (if (buffer-modified-p *twelf-config-buffer*)
- (progn
- (display-buffer *twelf-config-buffer*)
- (if (yes-or-no-p "Config buffer has changed, save new version? ")
- (save-buffer)
- (message "Checking old configuration"))))
- (if (not (verify-visited-file-modtime *twelf-config-buffer*))
- (if (yes-or-no-p "Config file has changed, read new contents? ")
- (revert-buffer t t)))
- (if (not (equal (visited-file-modtime) *twelf-config-time*))
- (progn
- (display-buffer *twelf-config-buffer*)
- (if (yes-or-no-p "Config file has changed, reconfigure server? ")
- (twelf-server-configure (buffer-file-name *twelf-config-buffer*)
- "Server OK: Configured")
- (if (not (yes-or-no-p "Ask next time? "))
- (setq *twelf-config-time* (visited-file-modtime))))))))
-
-(defun twelf-get-server-buffer (&optional createp)
- "Get the current Twelf server buffer.
-Optional argument CREATEP indicates if the buffer should be
-created if it doesn't exist."
- (if (and (bufferp *twelf-server-buffer*)
- (not (null (buffer-name *twelf-server-buffer*))))
- *twelf-server-buffer*
- (if createp
- (let ((twelf-server-buffer
- (get-buffer-create *twelf-server-buffer-name*)))
- (save-window-excursion
- (set-buffer twelf-server-buffer)
- (twelf-server-mode)
- (setq *twelf-server-buffer* twelf-server-buffer))
- twelf-server-buffer)
- (error "No Twelf server buffer"))))
-
-(defun twelf-init-variables ()
- "Initialize variables that track Twelf server state."
- (setq twelf-chatter 3)
- ;;(setq twelf-trace 0)
- (setq twelf-double-check "false")
- (setq twelf-print-implicit "false"))
-
-(defun twelf-server (&optional program)
- "Start an Twelf server process in a buffer named *twelf-server*.
-Any previously existing process is deleted after confirmation.
-Optional argument PROGRAM defaults to the value of the variable
-twelf-server-program.
-This locally re-binds `twelf-server-timeout' to 15 secs."
- (interactive)
- (let* ((default-program (if (null program) twelf-server-program program))
- (default-dir (file-name-directory default-program))
- (program (expand-file-name
- (if (null program)
- (read-file-name (concat "Twelf server: (default "
- (file-name-nondirectory
- default-program)
- ") ")
- default-dir
- default-program
- t)
- program)))
- ;; longer timeout during startup
- (twelf-server-timeout 15))
- ;; We save the program name as the default for the next time a server is
- ;; started in this session.
- (setq twelf-server-program program))
- (save-window-excursion
- (let* ((twelf-server-buffer (twelf-get-server-buffer t))
- (twelf-server-process (get-buffer-process twelf-server-buffer)))
- (set-buffer twelf-server-buffer)
- (if (not (null twelf-server-process))
- (if (yes-or-no-p "Kill current server process? ")
- (delete-process twelf-server-process)
- (error "Twelf Server restart aborted")))
- (goto-char (point-max))
- (setq *twelf-server-last-process-mark* (point))
- ;; initialize variables
- (twelf-init-variables)
- (start-process *twelf-server-process-name*
- twelf-server-buffer
- twelf-server-program)
- (twelf-server-wait)
- (twelf-server-process))))
-
-(defun twelf-server-process (&optional buffer)
- "Return the twelf server process, starting one if none exists."
- (let* ((twelf-server-buffer (if (null buffer) (twelf-get-server-buffer t)
- buffer))
- (twelf-server-process (get-buffer-process twelf-server-buffer)))
- (if (not (null twelf-server-process))
- twelf-server-process
- (twelf-server))))
-
-(defun twelf-server-display (&optional selectp)
- "Display Twelf server buffer, moving to the end of output.
-With prefix argument also selects the Twelf server buffer."
- (interactive "P")
- (display-server-buffer)
- (if selectp (pop-to-buffer (twelf-get-server-buffer))))
-
-(defun display-server-buffer (&optional buffer)
- "Display the Twelf server buffer so that the end of output is visible."
- (let* ((twelf-server-buffer (if (null buffer) (twelf-get-server-buffer)
- buffer))
- (_ (set-buffer twelf-server-buffer))
- (twelf-server-process (twelf-server-process twelf-server-buffer))
- (proc-mark (process-mark twelf-server-process))
- (_ (display-buffer twelf-server-buffer))
- (twelf-server-window (get-buffer-window twelf-server-buffer)))
- (if (not (pos-visible-in-window-p proc-mark twelf-server-window))
- (progn
- (push-mark proc-mark)
- (set-window-point twelf-server-window proc-mark)))
- (sit-for 0)))
-
-(defun twelf-server-send-command (command)
- "Send a string COMMAND to the Twelf server."
- (interactive "sCommand: ")
- (let* ((input (concat command "\n"))
- (twelf-server-buffer (twelf-get-server-buffer))
- (twelf-server-process (twelf-server-process twelf-server-buffer)))
- (if twelf-server-echo-commands
- (let ((previous-buffer (current-buffer)))
- (if twelf-server-display-commands
- (display-server-buffer twelf-server-buffer))
- (set-buffer twelf-server-buffer)
- (goto-char (point-max))
- (insert input)
- (set-marker (process-mark twelf-server-process) (point-max))
- (setq *twelf-error-pos* (point-max))
- (set-buffer previous-buffer)))
- (setq *twelf-last-input-buffer* twelf-server-buffer)
- (setq *twelf-server-last-process-mark*
- (marker-position (process-mark twelf-server-process)))
- (comint-send-string twelf-server-process input)))
-
-(defun twelf-accept-process-output (process timeout)
- "Incompatibility workaround for versions of accept-process-output.
-In case the function accepts no TIMEOUT argument, we wait potentially
-forever (until the user aborts, typically with \\[keyboard-quit])."
- (condition-case nil ; do not keep track of error message
- (accept-process-output process timeout)
- (wrong-number-of-arguments
- (accept-process-output process))))
-
-(defun twelf-server-wait (&optional displayp ok-message abort-message)
- "Wait for server acknowledgment and beep if error occurred.
-If optional argument DISPLAYP is non-NIL, or if an error occurred, the
-Twelf server buffer is displayed. Optional second and third arguments
-OK-MESSAGE and ABORT-MESSAGE are the strings to show upon successful
-completion or abort of the server which default to \"Server OK\" and
-\"Server ABORT\"."
- (let* ((chunk-count 0)
- (last-point *twelf-server-last-process-mark*)
- (previous-buffer (current-buffer))
- (previous-match-data (match-data))
- (twelf-server-buffer (twelf-get-server-buffer))
- (twelf-server-process (get-buffer-process twelf-server-buffer)))
- (unwind-protect
- (catch 'done
- (set-buffer twelf-server-buffer)
- (while t
- (goto-char last-point)
- (if (re-search-forward "\\(%% OK %%\n\\)\\|\\(%% ABORT %%\n\\)"
- (point-max) 'limit)
- (cond ((match-beginning 1)
- (if displayp
- (display-server-buffer twelf-server-buffer))
- (message (or ok-message "Server OK"))
- (throw 'done nil))
- ((match-beginning 2)
- (display-server-buffer twelf-server-buffer)
- (error (or abort-message "Server ABORT"))
- (throw 'done nil)))
- (cond ((or (not (twelf-accept-process-output
- twelf-server-process twelf-server-timeout))
- (= last-point (point)))
- (display-server-buffer twelf-server-buffer)
- (message "Server TIMEOUT, continuing Emacs")
- (throw 'done nil))
- (t (setq chunk-count (+ chunk-count 1))
- (if (= (mod chunk-count 10) 0)
- (message (make-string (/ chunk-count 10) ?#)))
- (sit-for 0))))))
- (store-match-data previous-match-data)
- (set-buffer previous-buffer))))
-
-(defun twelf-server-quit ()
- "Kill the Twelf server process."
- (interactive)
- (twelf-server-send-command "OS.exit"))
-
-(defun twelf-server-interrupt ()
- "Interrupt the Twelf server process."
- (interactive)
- (interrupt-process (twelf-server-process)))
-
-(defun twelf-reset ()
- "Reset the global signature of Twelf maintained by the server."
- (interactive)
- (twelf-server-send-command "reset"))
-
-(defun twelf-config-directory ()
- "Returns directory with current Twelf server configuration."
- (let ((config-file (buffer-file-name *twelf-config-buffer*)))
- (file-name-directory config-file)))
-
-;(defun relativize-file-name (filename dir)
-; "Relativize FILENAME with respect to DIR, if possible."
-; (if (string= dir (file-name-directory filename))
-; (file-name-nondirectory filename)
-; filename))
-
-(defun twelf-server-configure (config-file &optional ok-message)
- "Initializes the Twelf server configuration from CONFIG-FILE.
-A configuration file is a list of relative file names in
-dependency order. Lines starting with % are treated as comments.
-Starts a Twelf servers if necessary."
- (interactive
- (list (if twelf-config-mode (buffer-file-name)
- (expand-file-name
- (read-file-name "Visit config file: (default sources.cfg) "
- default-directory
- (concat default-directory "sources.cfg")
- nil ; don't require match for now
- )))))
- (let* ((config-file (if (file-directory-p config-file)
- (concat config-file "sources.cfg")
- config-file))
- (config-file-os (twelf-convert-standard-filename config-file))
- (config-dir (file-name-directory config-file))
- (config-dir-os (twelf-convert-standard-filename config-dir))
- (config-buffer (set-buffer (or (get-file-buffer config-file)
- (find-file-noselect config-file))))
- config-list)
- (setq *twelf-config-buffer* config-buffer)
- (if (and (not (verify-visited-file-modtime (get-file-buffer config-file)))
- (yes-or-no-p "Config file has changed, read new contents? "))
- (revert-buffer t t))
- (setq config-list (twelf-server-read-config))
- (twelf-server-process) ; Start process if necessary
- (let* ((_ (set-buffer (twelf-get-server-buffer)))
- (cd-command
- (if (equal default-directory config-dir)
- nil
- (setq default-directory config-dir)
- (concat "OS.chDir " config-dir-os)))
- (_ (set-buffer config-buffer)))
- (cond ((not (null cd-command))
- (twelf-server-send-command cd-command)
- (twelf-server-wait nil ""
- "Server ABORT: Could not change directory")))
- (twelf-server-send-command
- (concat "Config.read " config-file-os))
- (twelf-server-wait nil (or ok-message "Server OK")
- "Server ABORT: Could not be configured")
- ;; *twelf-config-buffer* should still be current buffer here
- (setq *twelf-config-time* (visited-file-modtime))
- (setq *twelf-config-list* config-list))))
-
-;(defun twelf-server-add-file (filename)
-; "Adds a file to the current configuration."
-; (interactive
-; (list (expand-file-name
-; (read-file-name "File to add: " (twelf-config-directory)))))
-; (let ((relative-file (file-relative-name filename (twelf-config-directory)))
-; temp-time)
-; (save-excursion
-; (set-buffer *twelf-config-buffer*)
-; (goto-char (point-max))
-; (if (not (= (point) (point-min)))
-; (progn
-; (backward-char 1)
-; (if (looking-at "\n")
-; (forward-char 1)
-; (forward-char 1)
-; (insert "\n"))))
-; (insert (concat relative-file "\n"))
-; (save-buffer)
-; (setq temp-time (visited-file-modtime)))
-; (twelf-server-send-command
-; (concat "Config.read " (buffer-file-name *twelf-config-buffer*)))
-; (twelf-server-wait nil "" "Server ABORT: File could not be added to
configuration")
-; (setq *twelf-config-list* (cons filename *twelf-config-list*))
-; (setq *twelf-config-time* temp-time)))
-
-(defun natp (x)
- "Checks if X is an integer greater or equal to 0."
- (and (integerp x) (>= x 0)))
-
-(defun twelf-read-nat ()
- "Reads a natural number from the minibuffer."
- (let ((num nil))
- (while (not (natp num))
- (setq num (read-from-minibuffer "Number: " (if num (prin1-to-string num))
- nil t t))
- (if (not (natp num)) (beep)))
- num))
-
-(defun twelf-read-bool ()
- "Read a boolean in mini-buffer."
- (completing-read "Boolean: "
- '(("true" . true) ("false" . false))
- nil t))
-
-(defun twelf-read-limit ()
- "Read a limit (* or natural number) in mini-buffer."
- (let ((input (read-string "Limit (* or nat): ")))
- (if (equal input "*")
- input
- (let ((n (string-to-number input)))
- (if (and (integerp n) (> n 0))
- n
- (error "Number must be non-negative integer"))))))
-
-(defun twelf-read-strategy ()
- "Read a strategy in mini-buffer."
- (completing-read "Strategy: "
- '(("FRS" . "FRS") ("RFS" . "RFS"))
- nil t))
-
-(defun twelf-read-value (argtype)
- "Call the read function appropriate for ARGTYPE and return result."
- (funcall (cdr (assoc argtype *twelf-read-functions*))))
-
-(defun twelf-set (parm value)
- "Sets the Twelf parameter PARM to VALUE.
-When called interactively, prompts for parameter and value, supporting
-completion."
- (interactive
- (let* ((parm (completing-read
- "Parameter: " *twelf-parm-table* nil t))
- (argtype (cdr (assoc parm *twelf-parm-table*)))
- (value (twelf-read-value argtype)))
- (list parm value)))
- (track-parm parm value) ; track, if necessary
- (twelf-server-send-command (concat "set " parm " " value)))
-
-(defun twelf-set-parm (parm)
- "Prompts for and set the value of Twelf parameter PARM.
-Used in menus."
- (let* ((argtype (cdr (assoc parm *twelf-parm-table*)))
- (value (and argtype (twelf-read-value argtype))))
- (if (null argtype)
- (error "Unknown parameter")
- (twelf-set parm value))))
-
-(defun track-parm (parm value)
- "Tracks Twelf parameter values in Emacs."
- (if (assoc parm *twelf-track-parms*)
- (set (cdr (assoc parm *twelf-track-parms*)) value)))
-
-(defun twelf-toggle-double-check ()
- "Toggles doubleCheck parameter of Twelf."
- (let ((value (if (string-equal twelf-double-check "false")
- "true" "false")))
- (twelf-set "doubleCheck" value)))
-
-(defun twelf-toggle-print-implicit ()
- "Toggles Print.implicit parameter of Twelf."
- (let ((value (if (string-equal twelf-print-implicit "false")
- "true" "false")))
- (twelf-set "Print.implicit" value)))
-
-(defun twelf-get (parm)
- "Prints the value of the Twelf parameter PARM.
-When called interactively, promts for parameter, supporting completion."
- (interactive (list (completing-read "Parameter: " *twelf-parm-table* nil t)))
- (twelf-server-send-command (concat "get " parm))
- (twelf-server-wait)
- (save-window-excursion
- (let ((twelf-server-buffer (twelf-get-server-buffer)))
- (set-buffer twelf-server-buffer)
- (goto-char *twelf-server-last-process-mark*)
- ;; We are now at the beginning of the output
- (end-of-line 1)
- (message (buffer-substring *twelf-server-last-process-mark* (point))))))
-
-(defun twelf-timers-reset ()
- "Reset the Twelf timers."
- (interactive)
- (twelf-server-send-command "Timers.reset"))
-
-(defun twelf-timers-show ()
- "Show and reset the Twelf timers."
- (interactive)
- (twelf-server-send-command "Timers.show")
- (twelf-server-wait t))
-
-(defun twelf-timers-check ()
- "Show the Twelf timers without resetting them."
- (interactive)
- (twelf-server-send-command "Timers.show")
- (twelf-server-wait t))
-
-(defun twelf-server-restart ()
- "Restarts server and re-initializes configuration.
-This is primarily useful during debugging of the Twelf server code or
-if the Twelf server is hopelessly wedged."
- (interactive)
- (twelf-server twelf-server-program)
- (twelf-server-configure (if *twelf-config-buffer*
- (buffer-file-name *twelf-config-buffer*)
- "sources.cfg")
- "Server configured, now checking...")
- (twelf-check-config))
-
-;;;----------------------------------------------------------------------
-;;; Twelf Config minor mode
-;;;----------------------------------------------------------------------
-
-(defun twelf-config-mode (&optional prefix)
- "Toggles minor mode for Twelf configuration files.
-This affects \\<twelf-mode-map>
- twelf-server-configure (\\[twelf-server-configure])
- twelf-save-check-config (\\[twelf-save-check-config])
-"
- (interactive "P")
- (make-local-variable 'twelf-config-mode)
- (cond ((not (assq 'twelf-config-mode minor-mode-alist))
- (setq minor-mode-alist
- (cons '(twelf-config-mode " Config") minor-mode-alist))))
- (cond ((or (not twelf-config-mode) prefix)
- (setq twelf-config-mode t)
- (run-hooks 'twelf-config-mode-hook))
- (t (setq twelf-config-mode t))))
-
-(defun twelf-config-mode-check (&optional buffer)
- "Switch on the Twelf Config minor mode if the ends in `.cfg'."
- (if (string-match "\\.cfg$" (buffer-file-name (or buffer (current-buffer))))
- (twelf-config-mode t)))
-
-;;;----------------------------------------------------------------------
-;;; Support for creating a TAGS file for current Twelf server configuration
-;;;----------------------------------------------------------------------
-
-(defun twelf-tag (&optional tags-filename)
- "Create tags file for current configuration.
-If the current configuration is sources.cfg, the tags file is TAGS.
-If current configuration is named FILE.cfg, tags file will be named FILE.tag
-Errors are displayed in the Twelf server buffer.
-Optional argument TAGS-FILENAME specifies alternative filename."
- (interactive)
- (twelf-server-sync-config)
- (let* ((error-buffer (twelf-get-server-buffer))
- (config-filename (buffer-file-name *twelf-config-buffer*))
- (tags-file
- (or tags-filename
- (if (string-equal "sources.cfg"
- (file-name-nondirectory config-filename))
- (concat (file-name-directory config-filename "TAGS"))
- (concat (file-name-sans-extension config-filename)
- ".tag")))))
- (save-excursion
- (set-buffer error-buffer)
- (goto-char (point-max))
- (insert "Tagging configuration " config-filename " in file " tags-file
"\n"))
- (set-buffer *twelf-config-buffer*)
- (twelf-tag-files (rev-relativize *twelf-config-list* default-directory)
- tags-file error-buffer)
- (if (get-buffer-process error-buffer)
- (set-marker (process-mark (get-buffer-process error-buffer))
- (point-max)))))
-
-(defun twelf-tag-files (filelist &optional tags-filename error-buffer)
- "Create tags file for FILELIST, routing errors to buffer *tags-errors*.
-Optional argument TAGS-FILENAME specifies alternative filename (default: TAGS),
-optional argument ERROR-BUFFER specifies alternative buffer for error message
-(default: *tags-errors*)."
- (let* ((tags-filename (or tags-filename "TAGS"))
- (tags-buffer (find-file-noselect tags-filename))
- (error-buffer (or error-buffer (new-temp-buffer "*tags-errors*"))))
- (save-excursion
- (set-buffer tags-buffer)
- (if (equal (point-min) (point-max))
- nil
- ;;(pop-to-buffer tags-buffer)
- ;;(if (yes-or-no-p "Delete current tags information? ")
- (delete-region (point-min) (point-max))
- ;;)
- ))
- (switch-to-buffer-other-window error-buffer)
- (while (not (null filelist))
- (twelf-tag-file (car filelist) tags-buffer error-buffer)
- (setq filelist (cdr filelist)))
- (save-excursion
- (set-buffer tags-buffer)
- (save-buffer))))
-
-(defun twelf-tag-file (filename tags-buffer error-buffer)
- "Deposit tag information for FILENAME in TAGS-BUFFER, errors in
ERROR-BUFFER."
- (let ((src-buffer (find-file-noselect filename))
- file-start file-end end-of-id tag-string)
- (save-excursion
- (set-buffer tags-buffer)
- (goto-char (point-max))
- (insert "\f\n" filename ",0\n")
- (setq file-start (point))
- (save-excursion
- (set-buffer src-buffer)
- (goto-char (point-min))
- (while (twelf-next-decl filename error-buffer)
- (setq end-of-id (point))
- (beginning-of-line 1)
- (setq tag-string
- (concat (buffer-substring (point) end-of-id)
- "\C-?" (current-line-absolute) "," (point) "\n"))
- (goto-char end-of-id)
- (if (not (twelf-end-of-par))
- (let ((error-line (current-line-absolute)))
- (save-excursion
- (set-buffer error-buffer)
- (goto-char (point-max))
- (insert filename ":" (int-to-string error-line)
- " Warning: missing period\n"))))
- (save-excursion
- (set-buffer tags-buffer)
- (insert tag-string))))
- (setq file-end (point-max))
- (goto-char (- file-start 2))
- (delete-char 1)
- (insert (int-to-string (- file-end file-start)))
- (goto-char (point-max)))))
-
-(defun twelf-next-decl (filename error-buffer)
- "Set point after the identifier of the next declaration.
-Return the declared identifier or `nil' if none was found.
-FILENAME and ERROR-BUFFER are used if something appears wrong."
- (let ((id nil)
- end-of-id
- beg-of-id)
- (skip-twelf-comments-and-whitespace)
- (while (and (not id) (not (eobp)))
- (setq beg-of-id (point))
- (if (zerop (skip-chars-forward *twelf-id-chars*))
- ;; Not looking at id: skip ahead
- (skip-ahead filename (current-line-absolute) "No identifier"
- error-buffer)
- (setq end-of-id (point))
- (skip-twelf-comments-and-whitespace)
- (if (not (looking-at ":"))
- ;; Not looking at valid decl: skip ahead
- (skip-ahead filename (current-line-absolute end-of-id) "No colon"
- error-buffer)
- (goto-char end-of-id)
- (setq id (buffer-substring beg-of-id end-of-id))))
- (skip-twelf-comments-and-whitespace))
- id))
-
-(defun skip-ahead (filename line message error-buffer)
- "Skip ahead when syntactic error was found.
-A parsable error message constited from FILENAME, LINE, and MESSAGE is
-deposited in ERROR-BUFFER."
- (if error-buffer
- (save-excursion
- (set-buffer error-buffer)
- (goto-char (point-max))
- (insert filename ":" (int-to-string line) " Warning: " message "\n")
- (setq *twelf-error-pos* (point))))
- (twelf-end-of-par))
-
-(defun current-line-absolute (&optional char-pos)
- "Return line number of CHAR-POS (default: point) in current buffer.
-Ignores any possible buffer restrictions."
- (1+ (count-lines 1 (or char-pos (point)))))
-
-(defun new-temp-buffer (&optional name)
- "Create or delete contents of buffer named \"*temp*\" and return it.
-Optional argument NAME specified an alternative name."
- (if (not name) (setq name "*temp*"))
- (if (get-buffer name)
- (save-excursion
- (set-buffer name)
- (delete-region (point-min) (point-max))
- (get-buffer name))
- (get-buffer-create name)))
-
-(defun rev-relativize (filelist dir)
- "Reverse and relativize FILELIST with respect to DIR."
- (let ((newlist nil))
- (while (not (null filelist))
- (setq newlist
- (cons (file-relative-name (car filelist) dir) newlist))
- (setq filelist (cdr filelist)))
- newlist))
-
-
-;;;----------------------------------------------------------------------
-;;; Twelf-SML mode
-;;;----------------------------------------------------------------------
-
-(defvar twelf-sml-mode-map nil
- "The keymap used in Twelf-SML mode.")
-
-(cond ((not twelf-sml-mode-map)
- ;;(setq twelf-sml-mode-map (full-copy-sparse-keymap comint-mode-map))
- ;; fixed for Emacs 19.25. -fp Thu Oct 27 09:08:44 1994
- (setq twelf-sml-mode-map (copy-keymap comint-mode-map))
- (install-basic-twelf-keybindings twelf-sml-mode-map)
- ))
-
-(defconst twelf-sml-prompt-regexp "^\\- \\|^\\?\\- ")
-
-(defun expand-dir (dir)
- "Expand argument and check that it is a directory."
- (let ((expanded-dir (file-name-as-directory (expand-file-name dir))))
- (if (not (file-directory-p expanded-dir))
- (error "%s is not a directory" dir))
- expanded-dir))
-
-(defun twelf-sml-cd (dir)
- "Make DIR become the Twelf-SML process' buffer's default directory and
-furthermore issue an appropriate command to the inferior Twelf-SML process."
- (interactive "DChange default directory: ")
- (let ((expanded-dir (expand-dir dir)))
- (save-excursion
- (set-buffer (twelf-sml-process-buffer))
- (setq default-directory expanded-dir)
- (comint-simple-send (twelf-sml-process) (concat "Twelf.OS.chDir \""
expanded-dir "\";")))
- ;;(pwd)
- ))
-
-(defconst twelf-sml-cd-regexp "^\\s *cd\\s *\"\\([^\"]*\\)\""
- "Regular expression used to match cd commands in Twelf-SML buffer.")
-
-(defun twelf-sml-directory-tracker (input)
- "Checks input for cd commands and changes default directory in buffer.
-As a side-effect, it sets *twelf-last-region-sent* to NIL to indicate
interactive
-input. As a second side-effect, it resets the *twelf-error-pos*.
-Used as comint-input-sentinel in Twelf-SML buffer."
- (if (twelf-input-filter input)
- (setq *twelf-last-region-sent* nil))
- (setq *twelf-last-input-buffer* (current-buffer))
- (setq *twelf-error-pos* (marker-position (process-mark (twelf-sml-process))))
- (cond ((string-match twelf-sml-cd-regexp input)
- (let ((expanded-dir (expand-dir (substring input
- (match-beginning 1)
- (match-end 1)))))
- (setq default-directory expanded-dir)
- (pwd)))))
-
-(defun twelf-sml-mode ()
- "Major mode for interacting with an inferior Twelf-SML process.
-
-The following commands are available:
-\\{twelf-sml-mode-map}
-
-An Twelf-SML process can be started with \\[twelf-sml].
-
-Customisation: Entry to this mode runs the hooks on twelf-sml-mode-hook.
-
-You can send queries to the inferior Twelf-SML process from other buffers.
-
-Commands:
-Return after the end of the process' output sends the text from the
- end of process to point.
-Return before the end of the process' output copies the current line
- to the end of the process' output, and sends it.
-Delete converts tabs to spaces as it moves back.
-Tab indents for Twelf; with argument, shifts rest
- of expression rigidly with the current line.
-C-M-q does Tab on each line starting within following expression.
-Paragraphs are separated only by blank lines. % start single comments,
-delimited comments are enclosed in %{...}%.
-If you accidentally suspend your process, use \\[comint-continue-subjob]
-to continue it."
- (interactive)
- (kill-all-local-variables)
- (comint-mode)
- (setq comint-prompt-regexp twelf-sml-prompt-regexp)
- (setq comint-input-filter 'twelf-input-filter)
- ;; changed for XEmacs 19.16 Sat Jun 13 11:28:53 1998
- (add-hook 'comint-input-filter-functions 'twelf-sml-directory-tracker
- nil t)
- (twelf-mode-variables)
-
- ;; For sequencing through error messages:
- (make-local-variable '*twelf-error-pos*)
- (setq *twelf-error-pos* (point-max))
- ;; Workaround for problem with Lucid Emacs version of comint.el:
- ;; must exclude double quotes " and must include $ and # in filenames.
- (make-local-variable 'comint-match-partial-pathname-chars)
- (setq comint-match-partial-pathname-chars
- "^][<>{}()!^&*\\|?`'\" \t\n\r\b")
-
- (setq major-mode 'twelf-sml-mode)
- (setq mode-name "Twelf-SML")
- (setq mode-line-process '(": %s"))
- (use-local-map twelf-sml-mode-map)
-
- (run-hooks 'twelf-sml-mode-hook))
-
-(defun twelf-sml (&optional cmd)
- "Run an inferior Twelf-SML process in a buffer *twelf-sml*.
-If there is a process already running in *twelf-sml*, just
-switch to that buffer. With argument, allows you to change the program
-which defaults to the value of twelf-sml-program. Runs the hooks from
-twelf-sml-mode-hook (after the comint-mode-hook is run).
-
-Type \\[describe-mode] in the process buffer for a list of commands."
- (interactive (list (and current-prefix-arg
- (read-string "Run Twelf-SML: " twelf-sml-program))))
- (let ((cmd (or cmd twelf-sml-program)))
- (cond ((not (comint-check-proc (twelf-sml-process-buffer)))
- ;; process does not already exist
- (set-buffer (apply 'make-comint "twelf-sml" cmd nil twelf-sml-args))
- ;; in case we are using SML mode (for error tracking)
- (if (boundp 'sml-buffer)
- (set 'sml-buffer (twelf-sml-process-buffer)))
- (twelf-sml-mode))))
- (switch-to-buffer (twelf-sml-process-buffer)))
-
-(defun switch-to-twelf-sml (eob-p)
- "Switch to the Twelf-SML process buffer.
-With argument, positions cursor at end of buffer."
- (interactive "P")
- (if (twelf-sml-process-buffer)
- (pop-to-buffer (twelf-sml-process-buffer))
- (error "No current process buffer. "))
- (cond (eob-p
- (push-mark)
- (goto-char (point-max)))))
-
-(defun display-twelf-sml-buffer (&optional buffer)
- "Display the Twelf-SML buffer so that the end of output is visible."
- ;; Accept output from Twelf-SML process
- (sit-for 1)
- (let* ((twelf-sml-buffer (if (null buffer) (twelf-sml-process-buffer)
- buffer))
- (_ (set-buffer twelf-sml-buffer))
- (twelf-sml-process (twelf-sml-process))
- (proc-mark (process-mark twelf-sml-process))
- (_ (display-buffer twelf-sml-buffer))
- (twelf-sml-window (get-buffer-window twelf-sml-buffer)))
- (if (not (pos-visible-in-window-p proc-mark twelf-sml-window))
- (progn
- (push-mark proc-mark)
- (set-window-point twelf-sml-window proc-mark)))))
-
-(defun twelf-sml-send-string (string)
- "Send the given string to the Twelf-SML process."
- (setq *twelf-last-input-buffer* (twelf-sml-process-buffer))
- (comint-send-string (twelf-sml-process) string))
-
-(defun twelf-sml-send-region (start end &optional and-go)
- "Send the current region to the inferior Twelf-SML process.
-Prefix argument means switch-to-twelf-sml afterwards.
-If the region is short, it is sent directly, via COMINT-SEND-REGION."
- (interactive "r\nP")
- (if (> start end)
- (twelf-sml-send-region end start and-go)
- ;; (setq twelf-sml-last-region-sent (list (current-buffer) start end))
- (let ((cur-buffer (current-buffer))
- (twelf-sml-buffer (twelf-sml-process-buffer)))
- (switch-to-buffer twelf-sml-buffer)
- ;; (setq sml-error-pos (marker-position (process-mark
(twelf-sml-process))))
- (setq *twelf-last-input-buffer* twelf-sml-buffer)
- (switch-to-buffer cur-buffer))
- (comint-send-region (twelf-sml-process) start end)
- (if (not (string= (buffer-substring (1- end) end) "\n"))
- (comint-send-string (twelf-sml-process) "\n"))
- ;; Next two lines mess up when an Twelf error occurs, since the
- ;; newline is not read and later messes up counting.
- ;; (if (not and-go)
- ;; (comint-send-string (twelf-sml-process) "\n"))
- (if and-go (switch-to-twelf-sml t)
- (if twelf-sml-display-queries (display-twelf-sml-buffer)))))
-
-(defun twelf-sml-send-query (&optional and-go)
- "Send the current declaration to the inferior Twelf-SML process as a query.
-Prefix argument means switch-to-twelf-sml afterwards."
- (interactive "P")
- (let* ((par (twelf-current-decl))
- (query-start (nth 0 par))
- (query-end (nth 1 par)))
- (twelf-sml-set-mode 'TWELF)
- (twelf-sml-send-region query-start query-end and-go)))
-
-(defun twelf-sml-send-newline (&optional and-go)
- "Send a newline to the inferior Twelf-SML process.
-If a prefix argument is given, switches to Twelf-SML buffer afterwards."
- (interactive "P")
- (twelf-sml-send-string "\n")
- (if and-go (switch-to-twelf-sml t)
- (if twelf-sml-display-queries (display-twelf-sml-buffer))))
-
-(defun twelf-sml-send-semicolon (&optional and-go)
- "Send a semi-colon to the inferior Twelf-SML process.
-If a prefix argument is given, switched to Twelf-SML buffer afterwards."
- (interactive "P")
- (twelf-sml-send-string ";\n")
- (if and-go (switch-to-twelf-sml t)
- (if twelf-sml-display-queries (display-twelf-sml-buffer))))
-
-(defun twelf-sml-status (&optional buffer)
- "Returns the status of the Twelf-SML process.
-This employs a heuristic, looking at the contents of the Twelf-SML buffer.
-Results:
- NONE --- no process
- ML --- ML top level
- TWELF --- Twelf top level
- MORE --- asking whether to find the next solution
- UNKNOWN --- process is running, but can't tell status."
- (let* ((twelf-sml-buffer (or buffer (twelf-sml-process-buffer)))
- (twelf-sml-process (get-buffer-process twelf-sml-buffer)))
- (if (null twelf-sml-process)
- 'NONE
- (save-excursion
- (set-buffer twelf-sml-buffer)
- (let ((buffer-end (buffer-substring (max (point-min) (- (point-max) 3))
- (point-max))))
- (cond ((string-match "\\?- " buffer-end) 'TWELF)
- ((string-match "\n- " buffer-end) 'ML)
- ((string-match "More\\? " buffer-end) 'MORE)
- (t 'UNKNOWN)))))))
-
-(defvar twelf-sml-init "Twelf.Config.load (Twelf.Config.read
\"sources.cfg\");\n"
- "Initial command sent to Twelf-SML process when started during
twelf-sml-set-mode 'TWELF.")
-
-(defun twelf-sml-set-mode (mode &optional buffer)
- "Attempts to read and if necessary correct the mode of the Twelf-SML buffer.
-This does not check if the status has been achieved. It returns NIL
-if the status is unknown and T if it believes the status should have
-been achieved. This allows for asynchronous operation."
- (cond
- ((eq mode 'ML)
- (let ((status (twelf-sml-status)))
- (cond ((eq status 'NONE) (twelf-sml) 't)
- ((eq status 'ML) 't)
- ((eq status 'TWELF) (twelf-sml-send-string "") 't)
- ((eq status 'MORE) (twelf-sml-send-string "q\n") 't)
- ((eq status 'UNKNOWN) nil))))
- ((eq mode 'TWELF)
- (let ((status (twelf-sml-status)))
- (cond ((eq status 'NONE)
- (twelf-sml)
- (twelf-sml-send-string twelf-sml-init)
- (twelf-sml-send-string "Twelf.top ();\n") 't)
- ((eq status 'ML)
- (twelf-sml-send-string "Twelf.top ();\n") 't)
- ((eq status 'TWELF) 't)
- ((eq status 'MORE) (twelf-sml-send-string "\n") 't)
- ((eq status 'UNKNOWN) nil))))
- (t (error "twelf-sml-set-mode: illegal mode %s" mode))))
-
-(defun twelf-sml-quit ()
- "Kill the Twelf-SML process."
- (interactive)
- (kill-process (twelf-sml-process)))
-
-(defun twelf-sml-process-buffer ()
- "Returns the current Twelf-SML process buffer."
- (get-buffer "*twelf-sml*"))
-
-(defun twelf-sml-process (&optional buffer)
- "Returns the current Twelf-SML process."
- (let ((proc (get-buffer-process (or buffer (twelf-sml-process-buffer)))))
- (or proc
- (error "No current process."))))
-
-;;;----------------------------------------------------------------------
-;;; 2Twelf-SML minor mode for Twelf
-;;; Some keybindings now refer to Twelf-SML instead of the Twelf server.
-;;; Toggle with twelf-to-twelf-sml-mode
-;;;----------------------------------------------------------------------
-
-(defvar twelf-to-twelf-sml-mode nil
- "Non-NIL means the minor mode is in effect.")
-
-(defun install-twelf-to-twelf-sml-keybindings (map)
- ;; Process commands:
- (define-key map "\C-c\C-r" 'twelf-sml-send-region)
- (define-key map "\C-c\C-e" 'twelf-sml-send-query)
- (define-key map "\C-c\C-m" 'twelf-sml-send-newline)
- (define-key map "\C-c\n" 'twelf-sml-send-newline)
- (define-key map "\C-c;" 'twelf-sml-send-semicolon)
- (define-key map "\C-cd" 'twelf-sml-cd)
- )
-
-(defvar twelf-to-twelf-sml-mode-map nil
- "Keymap for twelf-to-twelf-sml minor mode.")
-
-(cond ((not twelf-to-twelf-sml-mode-map)
- (setq twelf-to-twelf-sml-mode-map (make-sparse-keymap))
- (install-basic-twelf-keybindings twelf-to-twelf-sml-mode-map)
- (install-twelf-keybindings twelf-to-twelf-sml-mode-map)
- ;; The next line shadows certain bindings to refer to
- ;; Twelf-SML instead of the Twelf server.
- (install-twelf-to-twelf-sml-keybindings twelf-to-twelf-sml-mode-map)))
-
-(defun twelf-to-twelf-sml-mode (&optional prefix)
- "Toggles minor mode for sending queries to Twelf-SML instead of Twelf server.
-Specifically: \\<twelf-to-twelf-sml-mode-map>
- \\[twelf-sml-send-query] (for sending queries),
- \\[twelf-sml-send-newline] (for sending newlines) and
- \\[twelf-sml-send-semicolon] (for sending `;')
-are rebound.
-
-Mode map
-========
-\\{twelf-to-twelf-sml-mode-map}
-"
- (interactive "P")
- (make-local-variable 'twelf-to-twelf-sml-mode)
- (cond ((not (assq 'twelf-to-twelf-sml-mode minor-mode-alist))
- (setq minor-mode-alist
- (cons '(twelf-to-twelf-sml-mode " 2Twelf-SML")
- minor-mode-alist))))
- (cond ((or (not twelf-to-twelf-sml-mode) prefix)
- (setq twelf-to-twelf-sml-mode t)
- (use-local-map twelf-to-twelf-sml-mode-map)
- (run-hooks 'twelf-to-twelf-sml-mode-hook))
- (t
- (setq twelf-to-twelf-sml-mode nil)
- (use-local-map twelf-mode-map))))
-
-;;;----------------------------------------------------------------------
-;;; Twelf mode menus
-;;; requires auc-menu utilities
-;;;----------------------------------------------------------------------
-
-(cond
- ((string-match "XEmacs" emacs-version) ;; XEmacs nee Lucid Emacs
- (defun radio (label callback condition)
- (vector label callback ':style 'radio ':selected condition))
- (defun toggle (label callback condition)
- (vector label callback ':style 'toggle ':selected condition))
- (defun disable-form (label callback condition)
- (vector label callback condition))
- )
- (t ;; FSF Emacs 19
- (defun radio (label callback condition)
- (vector label callback t))
- (defun toggle (label callback condition)
- (vector label callback t))
- (defun disable-form (label callback condition)
- (cond ((symbolp condition) (vector label callback condition))
- (t (vector label callback t))))
- ))
-
-(defconst twelf-at-point-menu
- '("At Point"
- ["Constant" twelf-type-const t]
- ;["Type" twelf-type-at-point nil] ;disabled for Twelf 1.2
- ;["Expected Type" twelf-expected-type-at-point nil] ;disabled
- ;["List Completions" twelf-completions-at-point nil] ;disabled
- ;["Complete" twelf-complete nil] ;disabled
- )
- "Menu for commands applying at point.")
-
-(defconst twelf-server-state-menu
- '("Server State"
- ["Configure" twelf-server-configure t]
- ["Interrupt" twelf-server-interrupt t]
- ["Reset" twelf-reset t]
- ["Start" twelf-server t]
- ["Restart" twelf-server-restart t]
- ["Quit" twelf-server-quit t])
- "Menu for commands affecting server state.")
-
-(defconst twelf-error-menu
- '("Error Tracking"
- ["Next" twelf-next-error t]
- ["Goto" twelf-goto-error t])
- "Menu for error commands.")
-
-(defconst twelf-tags-menu
- '("Tags"
- ["Find" find-tag t]
- ["Find Other Window" find-tag-other-window t]
- ["Query Replace" tags-query-replace t]
- ["Search" tags-search t]
- ["Continue" tags-loop-continue t]
- ["Create/Update" twelf-tag t])
- "Menu for tag commands.")
-
-(defun twelf-toggle-server-display-commands ()
- (setq twelf-server-display-commands (not twelf-server-display-commands)))
-
-(defconst twelf-options-menu
- `("Options"
- (, (toggle "Display Commands" '(twelf-toggle-server-display-commands)
- 'twelf-server-display-commands))
- ("chatter"
- (, (radio "0" '(twelf-set "chatter" 0) '(= twelf-chatter 0)))
- (, (radio "1" '(twelf-set "chatter" 1) '(= twelf-chatter 1)))
- (, (radio "2" '(twelf-set "chatter" 2) '(= twelf-chatter 2)))
- (, (radio "3*" '(twelf-set "chatter" 3) '(= twelf-chatter 3)))
- (, (radio "4" '(twelf-set "chatter" 4) '(= twelf-chatter 4)))
- (, (radio "5" '(twelf-set "chatter" 5) '(= twelf-chatter 5)))
- (, (radio "6" '(twelf-set "chatter" 6) '(= twelf-chatter 6))))
- (, (toggle "doubleCheck" '(twelf-toggle-double-check)
- '(string-equal twelf-double-check "true")))
- ("Print."
- (, (toggle "implicit" '(twelf-toggle-print-implicit)
- '(string-equal twelf-print-implicit "true")))
- ["depth" (twelf-set-parm "Print.depth") t]
- ["length" (twelf-set-parm "Print.length") t]
- ["indent" (twelf-set-parm "Print.indent") t]
- ["width" (twelf-set-parm "Print.width") t])
- ("Prover."
- ["strategy" (twelf-set-parm "Prover.strategy") t]
- ["maxSplit" (twelf-set-parm "Prover.maxSplit") t]
- ["maxRecurse" (twelf-set-parm "Prover.maxRecurse") t])
- ;;["Trace" nil nil]
- ;; (, (radio "0" '(twelf-set "trace" 0) '(= twelf-trace 0)))
- ;; (, (radio "1" '(twelf-set "trace 1) '(= twelf-trace 1)))
- ;; (, (radio "2" '(twelf-set "trace" 2) '(= twelf-trace 2))))
- ;;["Untrace" nil nil]
- ;;(, (disable-form "Untrace" '(twelf-set "trace" 0)
- ;; '(not (= twelf-trace 0))))
- ["Reset Menubar" twelf-reset-menu t])
- "Menu to change options in Twelf mode.")
-
-(defconst twelf-timers-menu
- '("Timing"
- ["Show and Reset" twelf-timers-show t]
- ["Check" twelf-timers-check t]
- ["Reset" twelf-timers-reset t]))
-
-;(autoload 'toggle-twelf-font-immediate "twelf-font"
-; "Toggle experimental immediate highlighting in font-lock mode.")
-(autoload 'twelf-font-fontify-decl "twelf-font"
- "Fontify current declaration using font-lock minor mode.")
-(autoload 'twelf-font-fontify-buffer "twelf-font"
- "Fontify current buffer using font-lock minor mode.")
-
-(defconst twelf-syntax-menu
- `("Syntax Highlighting"
- ["Highlight Declaration" twelf-font-fontify-decl t]
- ["Highlight Buffer" twelf-font-fontify-buffer t]
- ;;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate
- ;;'font-lock-mode))
- )
- "Menu for syntax highlighting in Twelf mode.")
-
-(easy-menu-define twelf-menu (list twelf-mode-map)
- "Menu for Twelf mode.
-This may be selected from the menubar. In XEmacs, also bound to Button3."
- (list
- "Twelf"
- ["Display Server" twelf-server-display t]
- ["Check Configuration" twelf-save-check-config t]
- ["Check File" twelf-save-check-file t]
- ["Check Declaration" twelf-check-declaration t]
- twelf-at-point-menu
- twelf-error-menu
- twelf-options-menu
- twelf-syntax-menu
- twelf-tags-menu
- twelf-timers-menu
- twelf-server-state-menu
- ["Info" twelf-info t]))
-
-(defun twelf-add-menu ()
- "Add Twelf menu to menubar."
- (easy-menu-add twelf-menu twelf-mode-map))
-
-(defun twelf-remove-menu ()
- "Remove Twelf menu from menubar."
- (easy-menu-remove twelf-menu))
-
-(defun twelf-reset-menu ()
- "Reset Twelf menu."
- (twelf-remove-menu)
- (twelf-add-menu))
-
-;;;----------------------------------------------------------------------
-;;; Twelf Server mode menu
-;;;----------------------------------------------------------------------
-
-(easy-menu-define twelf-server-menu (list twelf-server-mode-map)
- "Menu for Twelf Server mode.
-This may be selected from the menubar. In XEmacs, also bound to Button3."
- (list
- "Twelf-Server"
- ;; ["Display Server" twelf-server-display t]
- ["Check Configuration" twelf-save-check-config t]
- ;; ["Check File" twelf-save-check-file nil]
- ;; ["Check Declaration" twelf-check-declaration nil]
- ;; ["Check Query" twelf-check-query nil]
- ;; ["Solve Query" twelf-solve-query nil]
- ;; ["At Point" () nil]
- twelf-error-menu
- twelf-options-menu
- twelf-tags-menu
- twelf-server-state-menu
- ["Info" twelf-info t]))
-
-(defun twelf-server-add-menu ()
- "Add Twelf menu to menubar."
- (easy-menu-add twelf-server-menu twelf-server-mode-map))
-
-(defun twelf-server-remove-menu ()
- "Remove Twelf menu from menubar."
- (easy-menu-remove twelf-server-menu))
-
-(defun twelf-server-reset-menu ()
- "Reset Twelf menu."
- (twelf-server-remove-menu)
- (twelf-server-add-menu))
-
-(provide 'twelf-old)
diff --git a/twelf/twelf.el b/twelf/twelf.el
deleted file mode 100644
index 236846f..0000000
--- a/twelf/twelf.el
+++ /dev/null
@@ -1,209 +0,0 @@
-;; twelf.el Proof General instance for Twelf
-;;
-;; Copyright (C) 2000 LFCS Edinburgh.
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
-;;
-;;
-;; TODO:
-;; Info doc menu entry
-;; X-Symbol upgrade/test? Mule XE better?
-;;
-
-
-(require 'proof-easy-config) ; easy configure mechanism
-
-(require 'twelf-font) ; font lock configuration
-;; (require 'twelf-old)
-;; FIXME: put parts of old code into twelf-syntax or similar
-
-;;
-;; User configuration settings for Twelf PG
-;;
-(defcustom twelf-root-dir
- "/usr/local/twelf/"
- "*Root of twelf installation. Default /usr/local/twelf suits RPM package."
- :type 'file
- :group 'twelf)
-
-(defcustom twelf-info-dir
- (concat twelf-root-dir "doc/info/")
- "*Directory of Twelf Infor files."
- :type 'file
- :group 'twelf)
-
-;;
-;; Instantiation of Proof General
-;;
-(proof-easy-config 'twelf "Twelf"
- proof-prog-name "twelf-server"
- proof-assistant-home-page "http://www.cs.cmu.edu/~twelf/";
-
- proof-terminal-char ?\.
- proof-script-comment-start "%" ;; for inserting comments
- proof-script-comment-end ""
- proof-script-comment-start-regexp "%[%{ \t\n\f]" ;; recognizing
- proof-script-comment-end-regexp "%}\\|\n" ;; comments
-
- proof-shell-auto-terminate-commands nil ; server commands don't end with .
- proof-shell-strip-crs-from-input nil ; server needs CRs with readDecl
-
- proof-auto-multiple-files t
- proof-shell-cd-cmd "OS.chDir %s"
- proof-shell-interrupt-regexp "interrupt"
-
- proof-shell-annotated-prompt-regexp "%% [OA][KB]O?R?T? %%\n"
- proof-shell-error-regexp "Server error:"
- proof-shell-quit-cmd "quit"
- proof-shell-restart-cmd "reset"
-
- ;; "Eager annotations" mark messages Proof General should display
- ;; or recognize while the prover is pontificating
- proof-shell-eager-annotation-start
- "^\\[Opening \\|\\[Closing "
- proof-shell-eager-annotation-end "\n"
-
- ;; next setting is just to prevent warning
- proof-save-command-regexp proof-no-regexp)
-
-
-;; unset: all of the interactive proof commands
-;; These don't really apply, I don't think, because Twelf
-;; only has fully automatic prover at the moment.
-;; Also, there is no concept of "undo" to remove declarations
-;; (can simply repeat them, tho.)
-;; 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
-;; proof-goal-command "%theorem %s."
-;; proof-save-command "%prove "
-;; remaining strings are left over from Isabelle example
-;; proof-kill-goal-command "Goal \"PROP no_goal_set\";"
-;; proof-showproof-command "pr()"
-;; proof-undo-n-times-cmd "pg_repeat undo %s;"
-;; proof-shell-start-goals-regexp "Level [0-9]"
-;; proof-shell-end-goals-regexp "val it"
-;; proof-shell-init-cmd
-;; proof-shell-proof-completed-regexp "^No subgoals!"
-
-
-;;
-;; Twelf server doesn't take declarations directly:
-;; we need to pre-process script input slightly
-;;
-
-(defun twelf-add-read-declaration ()
- "A hook value for `proof-shell-insert-hook'."
- (if (eq action 'proof-done-advancing)
- (setq string (concat "readDecl\n" string))))
-
-(add-hook 'proof-shell-insert-hook 'twelf-add-read-declaration)
-
-
-;;
-;; Syntax table
-;;
-
-;; Taken from old Emacs mode, renamed fns to be convention compliant
-(defun twelf-set-syntax (char entry)
- (modify-syntax-entry char entry twelf-mode-syntax-table))
-(defun twelf-set-word (char) (twelf-set-syntax char "w "))
-(defun twelf-set-symbol (char) (twelf-set-syntax char "_ "))
-
-(defun twelf-map-string (func string)
- (if (string= "" string)
- ()
- (funcall func (string-to-char string))
- (twelf-map-string func (substring string 1))))
-
-;; A-Z and a-z are already word constituents
-;; For fontification, it would be better if _ and ' were word constituents
-(twelf-map-string
- 'twelf-set-word "!&$^+/<=>?@~|#*`;,-0123456789\\") ; word constituents
-(twelf-map-string 'twelf-set-symbol "_'") ; symbol constituents
-;; Delimited comments are %{ }%, see 1234 below.
-(twelf-set-syntax ?\ " ") ; whitespace
-(twelf-set-syntax ?\t " ") ; whitespace
-; da: this old entry is wrong: it says % always starts a comment
-;(twelf-set-syntax ?% "< 14") ; comment begin
-; This next one is much better,
-(twelf-set-syntax ?% ". 14") ; comment begin/second char
-(twelf-set-syntax ?\n "> ") ; comment end
-(twelf-set-syntax ?: ". ") ; punctuation
-(twelf-set-syntax ?. ". ") ; punctuation
-(twelf-set-syntax ?\( "() ") ; open delimiter
-(twelf-set-syntax ?\) ")( ") ; close delimiter
-(twelf-set-syntax ?\[ "(] ") ; open delimiter
-(twelf-set-syntax ?\] ")[ ") ; close delimiter
-;(twelf-set-syntax ?\{ "(}2 ") ; open delimiter
-;(twelf-set-syntax ?\} "){ 3") ; close delimiter
-;; Actually, strings are illegal but we include:
-(twelf-set-syntax ?\" "\" ") ; string quote
-;; \ is not an escape, but a word constituent (see above)
-;;(twelf-set-syntax ?\\ "/ ") ; escape
-
-
-
-;;
-;; Syntax highlighting (from twelf-old.el, NEEDS WORK)
-;;
-;; Highlighting is maybe a nuisance for twelf because of its funny syntax.
-;; But font lock could perhaps be got to work with recent versions.
-;; That would be better than the present mechanism, which doesn't lock,
-;; doesn't work well with X Symbol (which really needs locking), and
-;; even breaks the background colouring for some reason (presumably
-;; the Twelf faces)
-
-(require 'twelf-font)
-(add-hook 'twelf-mode-hook 'twelf-mode-extra-config)
-
-(defun twelf-mode-extra-config ()
- (make-local-hook 'font-lock-after-fontify-buffer-hook)
- (add-hook 'font-lock-after-fontify-buffer-hook
- 'twelf-font-fontify-buffer nil 'local)
- (font-lock-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.")
-
-
-;;
-;; Setting Twelf options via Proof General
-;;
-
-(defpacustom chatter 1
- "Value for chatter."
- :type 'integer
- :setting "set chatter %i")
-
-(defpacustom double-check nil
- "Double-check declarations after type reconstruction."
- :type 'boolean
- :setting "set doubleCheck %b")
-(defpacustom print-implicit nil
- "Show implicit arguments."
- :type 'boolean
- :setting "set Print.implict %b")
-
-;; etc
-
-
-;;
-;; Twelf menu
-;;
-
-(defpgdefault menu-entries
- (cdr twelf-syntax-menu))
-
-
-(provide 'twelf)
- [nongnu] elpa/proof-general updated (20412f1 -> 1b1083e), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 1931c8c 01/13: Remove Twelf support,
ELPA Syncer <=
- [nongnu] elpa/proof-general 48bd86b 02/13: Remove HOL98 support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 73571a5 03/13: Remove CCC support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 8b16d1d 04/13: Remove LEGO support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 23f7895 05/13: Remove Hol-Light support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 6c9c995 12/13: Change the license to GPLv3+ (Fix #198), ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 511226f 09/13: Remove Isabelle/Isar support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 497709f 10/13: AUTHORS: Add notes about copyright status, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general 0a295cd 07/13: Remove Plastic support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general e27b1ef 08/13: Remove Lambda-Clam support, ELPA Syncer, 2021/11/25
- [nongnu] elpa/proof-general f99cdf2 11/13: Misc cosmetic tweaks that occurred during GPLv3+ license work, ELPA Syncer, 2021/11/25