diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-05 15:46:41 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-05 15:46:41 +0000 |
| commit | 8bbd767323c5fc14e5f22991e2c800dffd6366da (patch) | |
| tree | dcd2978a2a3de21c8f202459fe91b940ddb76eb1 /lego | |
| parent | 8e87e720fb393c4d1748f7aedbe366cd12f6770e (diff) | |
completed chapter on LEGO Proof General
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 31 |
1 files changed, 5 insertions, 26 deletions
diff --git a/lego/lego.el b/lego/lego.el index 72b81f0b..04f02224 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -25,7 +25,7 @@ ;; I believe this is standard for Linux under RedHat -tms (defcustom lego-tags "/usr/lib/lego/lib_Type/" - "*the default TAGS table for the LEGO library" + "*The directory of the TAGS table for the LEGO library" :type 'file :group 'lego) @@ -89,7 +89,7 @@ :group 'lego) (defcustom lego-www-latest-release - "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3/" + "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3.1/" "The WWW address for the latest LEGO release." :type 'string :group 'lego) @@ -107,17 +107,6 @@ :group 'lego) -;; ----- legostat and legogrep, courtesy of Mark Ruys - -(defvar legogrep-command (concat "legogrep -n \"\" " lego-test-all-name) - "Last legogrep command used in \\{legogrep}; default for next legogrep.") - -(defvar legostat-command "legostat -t") - -(defvar legogrep-regexp-alist - '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) - "Regexp used to match legogrep hits. See `compilation-error-regexp-alist'.") - ;; ----- lego-shell configuration options (defvar lego-prog-name "lego" @@ -297,11 +286,6 @@ (defun lego-state-preserving-p (cmd) (not (string-match lego-undoable-commands-regexp cmd))) -(defun lego-retract-command (file) - "LEGO command to retract file." - (concat "ForgetMark file " - (file-name-sans-extension (file-name-nondirectory file)))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Commands specific to lego ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -522,14 +506,9 @@ We assume that module identifiers coincide with file names." proof-shell-retract-files-regexp "forgot back through Mark \"\\(.*\\)\"" - ;;FIXME: we ought to set up separate font-lock instructions for - ;;the response, the goal buffer and the script - font-lock-keywords lego-font-lock-keywords-1) - -;; FIXME: da: I've removed this, I think fset is bad and proof-retract-command -;; doesn't seem to exist. -;; (fset 'proof-retract-command 'lego-retract-command) - (setq proof-shell-compute-new-files-list + font-lock-keywords lego-font-lock-keywords-1 + + proof-shell-compute-new-files-list 'lego-shell-compute-new-files-list) (lego-init-syntax-table) |